Let x0 of type ι be given.
Let x1 of type ο be given.
Assume H1: ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ (x2 = x3 ⟶ ∀ x5 : ο . x5) ⟶ (x2 = x4 ⟶ ∀ x5 : ο . x5) ⟶ (x3 = x4 ⟶ ∀ x5 : ο . x5) ⟶ (∀ x5 . x5 ∈ x0 ⟶ ∀ x6 : ι → ο . x6 x2 ⟶ x6 x3 ⟶ x6 x4 ⟶ x6 x5) ⟶ x1.
Apply unknownprop_fc646236ea6fa2c5216d8ec2e38d12566b66120d90466cea118f2d1bb5862799 with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
Let x2 of type ι be given.
Assume H2:
(λ x3 . and (x3 ∈ x0) (∃ x4 . and (x4 ∈ x0) (∃ x5 . and (x5 ∈ x0) (and (and (and (x3 = x4 ⟶ ∀ x6 : ο . x6) (x3 = x5 ⟶ ∀ x6 : ο . x6)) (x4 = x5 ⟶ ∀ x6 : ο . x6)) (∀ x6 . x6 ∈ x0 ⟶ or (or (x6 = x3) (x6 = x4)) (x6 = x5)))))) x2.
Apply H2 with
x1.
Assume H3: x2 ∈ x0.
Assume H4:
∃ x3 . and (x3 ∈ x0) (∃ x4 . and (x4 ∈ x0) (and (and (and (x2 = x3 ⟶ ∀ x5 : ο . x5) (x2 = x4 ⟶ ∀ x5 : ο . x5)) (x3 = x4 ⟶ ∀ x5 : ο . x5)) (∀ x5 . x5 ∈ x0 ⟶ or (or (x5 = x2) (x5 = x3)) (x5 = x4)))).
Apply H4 with
x1.
Let x3 of type ι be given.
Assume H5:
(λ x4 . and (x4 ∈ x0) (∃ x5 . and (x5 ∈ x0) (and (and (and (x2 = x4 ⟶ ∀ x6 : ο . x6) (x2 = x5 ⟶ ∀ x6 : ο . x6)) (x4 = x5 ⟶ ∀ x6 : ο . x6)) (∀ x6 . x6 ∈ x0 ⟶ or (or (x6 = x2) (x6 = x4)) (x6 = x5))))) x3.
Apply H5 with
x1.
Assume H6: x3 ∈ x0.
Assume H7:
∃ x4 . and (x4 ∈ x0) (and (and (and (x2 = x3 ⟶ ∀ x5 : ο . x5) (x2 = x4 ⟶ ∀ x5 : ο . x5)) (x3 = x4 ⟶ ∀ x5 : ο . x5)) (∀ x5 . x5 ∈ x0 ⟶ or (or (x5 = x2) (x5 = x3)) (x5 = x4))).
Apply H7 with
x1.
Let x4 of type ι be given.
Assume H8:
(λ x5 . and (x5 ∈ x0) (and (and (and (x2 = x3 ⟶ ∀ x6 : ο . x6) (x2 = x5 ⟶ ∀ x6 : ο . x6)) (x3 = x5 ⟶ ∀ x6 : ο . x6)) (∀ x6 . x6 ∈ x0 ⟶ or (or (x6 = x2) (x6 = x3)) (x6 = x5)))) x4.