Let x0 of type ι be given.
Let x1 of type ι → ι be given.
Assume H0: ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x1 x2 ⟶ x4 ∈ x1 x3 ⟶ x2 = x3.
Let x2 of type ο be given.
Assume H1:
∀ x3 : ι → ι . bij (lam x0 (λ x4 . x1 x4)) (famunion x0 (λ x4 . x1 x4)) x3 ⟶ x2.
Apply H1 with
λ x3 . ap x3 1.
Apply bijI with
lam x0 (λ x3 . x1 x3),
famunion x0 (λ x3 . x1 x3),
λ x3 . ap x3 1 leaving 3 subgoals.
Let x3 of type ι be given.
Assume H2:
x3 ∈ lam x0 (λ x4 . x1 x4).
Apply famunionI with
x0,
x1,
ap x3 0,
ap x3 1 leaving 2 subgoals.
Apply ap0_Sigma with
x0,
x1,
x3.
The subproof is completed by applying H2.
Apply ap1_Sigma with
x0,
x1,
x3.
The subproof is completed by applying H2.
Let x3 of type ι be given.
Assume H2:
x3 ∈ lam x0 (λ x4 . x1 x4).
Let x4 of type ι be given.
Assume H3:
x4 ∈ lam x0 (λ x5 . x1 x5).
Assume H4:
ap x3 1 = ap x4 1.
Apply tuple_Sigma_eta with
x0,
x1,
x3,
λ x5 x6 . x5 = x4 leaving 2 subgoals.
The subproof is completed by applying H2.
Apply tuple_Sigma_eta with
x0,
x1,
x4,
λ x5 x6 . lam 2 (λ x7 . If_i (x7 = 0) (ap x3 0) (ap x3 1)) = x5 leaving 2 subgoals.
The subproof is completed by applying H3.
Claim L5:
ap x3 0 = ap x4 0Apply H0 with
ap x3 0,
ap x4 0,
ap x3 1 leaving 4 subgoals.
Apply ap0_Sigma with
x0,
x1,
x3.
The subproof is completed by applying H2.
Apply ap0_Sigma with
x0,
x1,
x4.
The subproof is completed by applying H3.
Apply ap1_Sigma with
x0,
x1,
x3.
The subproof is completed by applying H2.
Apply H4 with
λ x5 x6 . x6 ∈ x1 (ap x4 0).
Apply ap1_Sigma with
x0,
x1,
x4.
The subproof is completed by applying H3.
Apply L5 with
λ x5 x6 . lam 2 (λ x7 . If_i (x7 = 0) x6 (ap x3 1)) = lam 2 (λ x7 . If_i (x7 = 0) (ap x4 0) (ap x4 1)).
Apply H4 with
λ x5 x6 . lam 2 (λ x7 . If_i (x7 = 0) (ap x4 0) x6) = lam 2 (λ x7 . If_i (x7 = 0) (ap x4 0) (ap x4 1)).
Let x5 of type ι → ι → ο be given.
Assume H6:
x5 (lam 2 (λ x6 . If_i (x6 = 0) (ap x4 0) (ap x4 1))) (lam 2 (λ x6 . If_i (x6 = 0) (ap x4 0) (ap x4 1))).
The subproof is completed by applying H6.
Let x3 of type ι be given.
Assume H2:
x3 ∈ famunion x0 (λ x4 . x1 x4).
Apply famunionE_impred with
x0,
x1,
x3,
∃ x4 . and (x4 ∈ lam x0 (λ x5 . x1 x5)) ((λ x5 . ap x5 1) x4 = ...) leaving 2 subgoals.