Let x0 of type ι → ο be given.
Assume H0: x0 1.
Let x1 of type ο be given.
Apply H1 with
1.
Let x2 of type ο be given.
Apply H2 with
λ x3 . lam x3 (λ x4 . 0).
Apply andI with
x0 1,
∀ x3 . x0 x3 ⟶ and (HomSet x3 1 (lam x3 (λ x4 . 0))) (∀ x4 . HomSet x3 1 x4 ⟶ x4 = lam x3 (λ x5 . 0)) leaving 2 subgoals.
The subproof is completed by applying H0.
Let x3 of type ι be given.
Assume H3: x0 x3.
Apply andI with
HomSet x3 1 (lam x3 (λ x4 . 0)),
∀ x4 . HomSet x3 1 x4 ⟶ x4 = lam x3 (λ x5 . 0) leaving 2 subgoals.
Apply lam_Pi with
x3,
λ x4 . 1,
λ x4 . 0.
Let x4 of type ι be given.
Assume H4: x4 ∈ x3.
The subproof is completed by applying In_0_1.
Let x4 of type ι be given.
Assume H4:
x4 ∈ Pi x3 (λ x5 . 1).
set y5 to be x4
set y6 to be
lam x4 (λ x6 . 0)Claim L5: ∀ x7 : ι → ο . x7 y6 ⟶ x7 y5
Let x7 of type ι → ο be given.
Assume H5:
x7 (lam y5 (λ x8 . 0)).
set y8 to be λ x8 . x7
Apply Pi_eta with
y5,
λ x9 . 1,
y6,
λ x9 x10 . y8 x10 x9 leaving 2 subgoals.
The subproof is completed by applying H4.
Apply encode_u_ext with
y6,
λ x9 . ap x7 x9,
λ x9 . 0,
λ x9 . y8 leaving 2 subgoals.
Let x9 of type ι be given.
Assume H6: x9 ∈ y6.
Apply SingE with
0,
ap x7 x9.
Apply eq_1_Sing0 with
λ x10 x11 . ap x7 x9 ∈ x10.
Apply ap_Pi with
y6,
λ x10 . 1,
x7,
x9 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H6.
The subproof is completed by applying H5.
Let x7 of type ι → ι → ο be given.
Apply L5 with
λ x8 . x7 x8 y6 ⟶ x7 y6 x8.
Assume H6: x7 y6 y6.
The subproof is completed by applying H6.