Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι → ι be given.
Assume H2:
∀ x3 . In x3 x1 ⟶ nat_p (x2 x3).
Apply unknownprop_e5301b3d70bda0519d63620f3030249cd4bf7b92497d8242491e59897566ec4b with
x0,
nat_p (famunion x1 (λ x3 . x2 x3)) leaving 2 subgoals.
The subproof is completed by applying H0.
Let x3 of type ι be given.
Apply andE with
nat_p x3,
equip (V_ x0) x3,
nat_p (famunion x1 (λ x4 . x2 x4)) leaving 2 subgoals.
The subproof is completed by applying H3.
Apply unknownprop_f82d0f217e1b2a36bc273d145ee21e9b9e753d654bb0c650cc08860c1b4bd1f0 with
x3,
V_ x0,
nat_p (famunion x1 (λ x4 . x2 x4)) leaving 2 subgoals.
Apply unknownprop_1b764290fde7c6be5dad24a6a257b6d0c773613bb687261020b529743ed07853 with
V_ x0,
x3.
The subproof is completed by applying H5.
Let x4 of type ι → ι be given.
Assume H6:
bij x3 (V_ x0) x4.
Apply unknownprop_db24d9aa1dc52b3c0eaf7cf69655226164a8ab5afc5d72e14a32016133f537ca with
x3,
V_ x0,
x4,
nat_p (famunion x1 (λ x5 . x2 x5)) leaving 2 subgoals.
The subproof is completed by applying H6.
Assume H7:
inj x3 (V_ x0) x4.
Apply unknownprop_6a8f953ba7c3bf327e583b76a91b24ddd499843a498fbfe2514e26f3800e68b3 with
x3,
V_ x0,
x4,
(∀ x5 . In x5 (V_ x0) ⟶ ∃ x6 . and (In x6 x3) (x4 x6 = x5)) ⟶ nat_p (famunion x1 (λ x5 . x2 x5)) leaving 2 subgoals.
The subproof is completed by applying H7.
Assume H8:
∀ x5 . In x5 x3 ⟶ In (x4 x5) (V_ x0).
Assume H9:
∀ x5 . In x5 x3 ⟶ ∀ x6 . In x6 x3 ⟶ x4 x5 = x4 x6 ⟶ x5 = x6.
Assume H10:
∀ x5 . In x5 (V_ x0) ⟶ ∃ x6 . and (In x6 x3) (x4 x6 = x5).
Apply L12 with
λ x5 x6 . nat_p x6.
Apply unknownprop_5eb8f500639a60e571bbbfe0e511fec5aa60f16371092e11923e95756a9de9db with
λ x5 . If_i (and (In x5 x3) (In (x4 x5) x1)) (x2 (x4 x5)) 0,
x3,
nat_p (famunion x3 (λ x5 . (λ x6 . If_i (and (In x6 x3) (In (x4 x6) x1)) (x2 (x4 x6)) 0) x5)) leaving 4 subgoals.
The subproof is completed by applying L11.
The subproof is completed by applying H4.
Assume H13: x3 = 0.
Claim L14:
famunion x3 (λ x5 . (λ x6 . If_i (and (In x6 x3) (In (x4 x6) x1)) (x2 (x4 x6)) 0) x5) = 0Apply H13 with
λ x5 x6 . famunion x6 (λ x7 . (λ x8 . If_i (and (In x8 x3) (In (x4 x8) x1)) (x2 (x4 x8)) 0) x7) = 0.
The subproof is completed by applying unknownprop_a742184fb628dd913a065a33315fb84c9da76d8f75b4f99153dc31349e98ec25 with
λ x5 . If_i (and (In x5 x3) (In (x4 x5) x1)) (x2 (x4 x5)) 0.
Apply L14 with
λ x5 x6 . nat_p x6.
The subproof is completed by applying unknownprop_0e150139fedb8d7a0ae85e3054b4c73c936e7acb880ce730fb00a0093c9c6c27.
Let x5 of type ι be given.
Assume H14:
∀ x6 . ... ⟶ Subq ((λ x7 . ...) ...) ....