Let x0 of type ι be given.
Let x1 of type ο be given.
Assume H1: ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ (x2 = x3 ⟶ ∀ x6 : ο . x6) ⟶ (x2 = x4 ⟶ ∀ x6 : ο . x6) ⟶ (x2 = x5 ⟶ ∀ x6 : ο . x6) ⟶ (x3 = x4 ⟶ ∀ x6 : ο . x6) ⟶ (x3 = x5 ⟶ ∀ x6 : ο . x6) ⟶ (x4 = x5 ⟶ ∀ x6 : ο . x6) ⟶ x1.
Apply unknownprop_95c6cbd2308b27a7edcd2a1d9389b377988e902d740d05dc7c88e6b8da945ab9 with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying L2.
Let x2 of type ι be given.
Assume H3: x2 ∈ x0.
Let x3 of type ι be given.
Assume H4: x3 ∈ x0.
Let x4 of type ι be given.
Assume H5: x4 ∈ x0.
Assume H6: x2 = x3 ⟶ ∀ x5 : ο . x5.
Assume H7: x2 = x4 ⟶ ∀ x5 : ο . x5.
Assume H8: x3 = x4 ⟶ ∀ x5 : ο . x5.
Apply xm with
∀ x5 : ο . (∀ x6 . x6 ∈ x0 ⟶ (x2 = x6 ⟶ ∀ x7 : ο . x7) ⟶ (x3 = x6 ⟶ ∀ x7 : ο . x7) ⟶ (x4 = x6 ⟶ ∀ x7 : ο . x7) ⟶ x5) ⟶ x5,
x1 leaving 2 subgoals.
Assume H9: ∀ x5 : ο . (∀ x6 . x6 ∈ x0 ⟶ (x2 = x6 ⟶ ∀ x7 : ο . x7) ⟶ (x3 = x6 ⟶ ∀ x7 : ο . x7) ⟶ (x4 = x6 ⟶ ∀ x7 : ο . x7) ⟶ x5) ⟶ x5.
Apply H9 with
x1.
Let x5 of type ι be given.
Assume H10: x5 ∈ x0.
Assume H11: x2 = x5 ⟶ ∀ x6 : ο . x6.
Assume H12: x3 = x5 ⟶ ∀ x6 : ο . x6.
Assume H13: x4 = x5 ⟶ ∀ x6 : ο . x6.
Apply H1 with
x2,
x3,
x4,
x5 leaving 10 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
The subproof is completed by applying H10.
The subproof is completed by applying H6.
The subproof is completed by applying H7.
The subproof is completed by applying H11.
The subproof is completed by applying H8.
The subproof is completed by applying H12.
The subproof is completed by applying H13.
Assume H9:
not (∀ x5 : ο . (∀ x6 . x6 ∈ x0 ⟶ (x2 = x6 ⟶ ∀ x7 : ο . x7) ⟶ (x3 = x6 ⟶ ∀ x7 : ο . x7) ⟶ (x4 = x6 ⟶ ∀ x7 : ο . x7) ⟶ x5) ⟶ x5).
Let x5 of type ο be given.
Assume H12:
∀ x6 : ι → ι . inj x0 u3 x6 ⟶ x5.
Apply H12 with
inv u3 (λ x6 . ap (lam 3 (λ x7 . If_i (x7 = 0) x2 (If_i (x7 = 1) x3 x4))) x6).
Apply andI with
∀ x6 . x6 ∈ x0 ⟶ inv u3 (λ x7 . ap (lam 3 (λ x8 . If_i (x8 = 0) x2 (If_i (x8 = 1) x3 x4))) x7) x6 ∈ u3,
∀ x6 . ... ⟶ ∀ x7 . ... ⟶ inv u3 (λ x8 . ap (lam 3 (λ x9 . If_i (x9 = 0) x2 (If_i (x9 = 1) x3 x4))) x8) x6 = inv u3 ... ... ⟶ x6 = x7 leaving 2 subgoals.
Apply FalseE with
x1.
Apply unknownprop_8a6bdce060c93f04626730b6e01b099cc0487102a697e253c81b39b9a082262d with
u3 leaving 2 subgoals.
The subproof is completed by applying nat_3.
Apply atleastp_tra with
u4,
x0,
u3 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L10.