Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H2:
∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x1 ⟶ ∃ x4 . and (x4 ∈ 3) (∃ x5 . and (x5 ∈ 3) (and (and (x4 = x5 ⟶ ∀ x6 : ο . x6) (x4 ∈ x2 = x4 ∈ x3)) (x5 ∈ x2 = x5 ∈ x3))).
Let x2 of type ο be given.
Apply xm with
∃ x3 . and (x3 ∈ x0) (∃ x4 . and (x4 ∈ x0) (x3 = x4 ⟶ ∀ x5 : ο . x5)),
x2 leaving 2 subgoals.
Assume H8:
∃ x3 . and (x3 ∈ x0) (∃ x4 . and (x4 ∈ x0) (x3 = x4 ⟶ ∀ x5 : ο . x5)).
Apply xm with
∃ x3 . and (x3 ∈ x1) (∃ x4 . and (x4 ∈ x1) (x3 = x4 ⟶ ∀ x5 : ο . x5)),
x2 leaving 2 subgoals.
Assume H9:
∃ x3 . and (x3 ∈ x1) (∃ x4 . and (x4 ∈ x1) (x3 = x4 ⟶ ∀ x5 : ο . x5)).
Apply H8 with
x2.
Let x3 of type ι be given.
Assume H10:
(λ x4 . and (x4 ∈ x0) (∃ x5 . and (x5 ∈ x0) (x4 = x5 ⟶ ∀ x6 : ο . x6))) x3.
Apply H10 with
x2.
Assume H11: x3 ∈ x0.
Assume H12:
∃ x4 . and (x4 ∈ x0) (x3 = x4 ⟶ ∀ x5 : ο . x5).
Apply H12 with
x2.
Let x4 of type ι be given.
Assume H13:
(λ x5 . and (x5 ∈ x0) (x3 = x5 ⟶ ∀ x6 : ο . x6)) x4.
Apply H13 with
x2.
Assume H14: x4 ∈ x0.
Assume H15: x3 = x4 ⟶ ∀ x5 : ο . x5.
Apply L16 with
x2.
Let x5 of type ι be given.
Assume H17:
(λ x6 . and (x6 ∈ x1) (∃ x7 . and (x7 ∈ x1) (and (x3 = x6 ⟶ ∀ x8 : ο . x8) (x6 = x7 ⟶ ∀ x8 : ο . x8)))) x5.
Apply H17 with
x2.
Assume H18: x5 ∈ x1.
Assume H19:
∃ x6 . and (x6 ∈ x1) (and (x3 = x5 ⟶ ∀ x7 : ο . x7) (x5 = x6 ⟶ ∀ x7 : ο . x7)).
Apply H19 with
x2.
Let x6 of type ι be given.
Assume H20:
(λ x7 . and (x7 ∈ x1) (and (x3 = x5 ⟶ ∀ x8 : ο . x8) (x5 = x7 ⟶ ∀ x8 : ο . x8))) x6.
Apply H20 with
x2.
Assume H21: x6 ∈ x1.
Assume H22:
and (x3 = x5 ⟶ ∀ x7 : ο . x7) (x5 = x6 ⟶ ∀ x7 : ο . x7).
Apply H22 with
x2.
Assume H23: x3 = x5 ⟶ ∀ x7 : ο . x7.
Assume H24: x5 = ... ⟶ ∀ x7 : ο . x7.