Let x0 of type ι → ο be given.
Assume H0: x0 0.
Let x1 of type ο be given.
Apply H1 with
0.
Let x2 of type ο be given.
Apply H2 with
λ x3 . lam 0 (λ x4 . 0).
Apply andI with
x0 0,
∀ x3 . x0 x3 ⟶ and (HomSet 0 x3 (lam 0 (λ x4 . 0))) (∀ x4 . HomSet 0 x3 x4 ⟶ x4 = lam 0 (λ 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 0 x3 (lam 0 (λ x4 . 0)),
∀ x4 . HomSet 0 x3 x4 ⟶ x4 = lam 0 (λ x5 . 0) leaving 2 subgoals.
Apply lam_Pi with
0,
λ x4 . x3,
λ x4 . 0.
Let x4 of type ι be given.
Assume H4: x4 ∈ 0.
Apply FalseE with
(λ x5 . 0) x4 ∈ (λ x5 . x3) x4.
Apply EmptyE with
x4.
The subproof is completed by applying H4.
Let x4 of type ι be given.
Assume H4:
x4 ∈ Pi 0 (λ x5 . x3).
set y5 to be x4
set y6 to be
lam 0 (λ x6 . 0)Claim L5: ∀ x7 : ι → ο . x7 y6 ⟶ x7 y5
Let x7 of type ι → ο be given.
Assume H5:
x7 (lam 0 (λ x8 . 0)).
set y8 to be λ x8 . x7
Apply Pi_eta with
0,
λ x9 . y5,
y6,
λ x9 x10 . y8 x10 x9 leaving 2 subgoals.
The subproof is completed by applying H4.
Apply encode_u_ext with
0,
λ x9 . ap x7 x9,
λ x9 . 0,
λ x9 . y8 leaving 2 subgoals.
Let x9 of type ι be given.
Assume H6: x9 ∈ 0.
Apply FalseE with
(λ x10 . ap x7 x10) x9 = (λ x10 . 0) x9.
Apply EmptyE with
x9.
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.