Let x0 of type ο be given.
Apply H0 with
pack_e 1 0.
Let x1 of type ο be given.
Apply H1 with
λ x2 . lam 1 (λ x3 . ap x2 1).
Apply andI with
struct_e (pack_e 1 0),
∀ x2 . struct_e x2 ⟶ and (PtdSetHom (pack_e 1 0) x2 (lam 1 (λ x3 . ap x2 1))) (∀ x3 . PtdSetHom (pack_e 1 0) x2 x3 ⟶ x3 = lam 1 (λ x4 . ap x2 1)) leaving 2 subgoals.
Apply pack_struct_e_I with
1,
0.
The subproof is completed by applying In_0_1.
Let x2 of type ι be given.
Apply H2 with
λ x3 . and (PtdSetHom (pack_e 1 0) x3 (lam 1 (λ x4 . ap x3 1))) (∀ x4 . PtdSetHom (pack_e 1 0) x3 x4 ⟶ x4 = lam 1 (λ x5 . ap x3 1)).
Let x3 of type ι be given.
Let x4 of type ι be given.
Assume H3: x4 ∈ x3.
Apply pack_e_1_eq2 with
x3,
x4,
λ x5 x6 . and (PtdSetHom (pack_e 1 0) (pack_e x3 x4) (lam 1 (λ x7 . x5))) (∀ x7 . PtdSetHom (pack_e 1 0) (pack_e x3 x4) x7 ⟶ x7 = lam 1 (λ x8 . x5)).
Apply andI with
PtdSetHom (pack_e 1 0) (pack_e x3 x4) (lam 1 (λ x5 . x4)),
∀ x5 . PtdSetHom (pack_e 1 0) (pack_e x3 x4) x5 ⟶ x5 = lam 1 (λ x6 . x4) leaving 2 subgoals.
Apply unknownprop_266cf3934e79ff708b43f6101066886a004a8b2cb57b38750ae943dbc174c7c9 with
1,
x3,
0,
x4,
lam 1 (λ x5 . x4),
λ x5 x6 : ο . x6.
Apply andI with
lam 1 (λ x5 . x4) ∈ setexp x3 1,
ap (lam 1 (λ x5 . x4)) 0 = x4 leaving 2 subgoals.
Apply lam_Pi with
1,
λ x5 . x3,
λ x5 . x4.
Let x5 of type ι be given.
Assume H4: x5 ∈ 1.
The subproof is completed by applying H3.
Apply beta with
1,
λ x5 . x4,
0.
The subproof is completed by applying In_0_1.
Let x5 of type ι be given.
Apply unknownprop_266cf3934e79ff708b43f6101066886a004a8b2cb57b38750ae943dbc174c7c9 with
1,
x3,
0,
x4,
x5,
λ x6 x7 : ο . x7 ⟶ x5 = lam 1 (λ x8 . x4).
Apply H4 with
x5 = lam 1 (λ x6 . x4).
set y6 to be ...
set y7 to be ...
Claim L7: ∀ x8 : ι → ο . x8 y7 ⟶ x8 y6
Let x8 of type ι → ο be given.
Assume H7:
x8 (lam 1 (λ x9 . y6)).
Let x8 of type ι → ι → ο be given.
Apply L7 with
λ x9 . x8 x9 y7 ⟶ x8 y7 x9.
Assume H8: x8 y7 y7.
The subproof is completed by applying H8.