Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Let x4 of type ι be given.
Let x5 of type ι → ι → ο be given.
Assume H3: ∀ x6 x7 . x5 x6 x7 ⟶ x5 x7 x6.
Apply H0 with
x5,
or (∃ x6 . and (x6 ⊆ x4) (and (atleastp x1 x6) (∀ x7 . x7 ∈ x6 ⟶ ∀ x8 . x8 ∈ x6 ⟶ (x7 = x8 ⟶ ∀ x9 : ο . x9) ⟶ x5 x7 x8))) (∃ x6 . and (x6 ⊆ x4) (and (atleastp x3 x6) (∀ x7 . x7 ∈ x6 ⟶ ∀ x8 . x8 ∈ x6 ⟶ (x7 = x8 ⟶ ∀ x9 : ο . x9) ⟶ not (x5 x7 x8)))) leaving 3 subgoals.
The subproof is completed by applying H3.
Assume H4:
∃ x6 . and (x6 ⊆ x4) (and (equip x0 x6) (∀ x7 . x7 ∈ x6 ⟶ ∀ x8 . x8 ∈ x6 ⟶ (x7 = x8 ⟶ ∀ x9 : ο . x9) ⟶ x5 x7 x8)).
Apply H4 with
or (∃ x6 . and (x6 ⊆ x4) (and (atleastp x1 x6) (∀ x7 . x7 ∈ x6 ⟶ ∀ x8 . x8 ∈ x6 ⟶ (x7 = x8 ⟶ ∀ x9 : ο . x9) ⟶ x5 x7 x8))) (∃ x6 . and (x6 ⊆ x4) (and (atleastp x3 x6) (∀ x7 . x7 ∈ x6 ⟶ ∀ x8 . x8 ∈ x6 ⟶ (x7 = x8 ⟶ ∀ x9 : ο . x9) ⟶ not (x5 x7 x8)))).
Let x6 of type ι be given.
Assume H5:
(λ x7 . and (x7 ⊆ x4) (and (equip x0 x7) (∀ x8 . x8 ∈ x7 ⟶ ∀ x9 . x9 ∈ x7 ⟶ (x8 = x9 ⟶ ∀ x10 : ο . x10) ⟶ x5 x8 x9))) x6.
Apply H5 with
or (∃ x7 . and (x7 ⊆ x4) (and (atleastp x1 x7) (∀ x8 . x8 ∈ x7 ⟶ ∀ x9 . x9 ∈ x7 ⟶ (x8 = x9 ⟶ ∀ x10 : ο . x10) ⟶ x5 x8 x9))) (∃ x7 . and (x7 ⊆ x4) (and (atleastp x3 x7) (∀ x8 . x8 ∈ x7 ⟶ ∀ x9 . x9 ∈ x7 ⟶ (x8 = x9 ⟶ ∀ x10 : ο . x10) ⟶ not (x5 x8 x9)))).
Assume H6: x6 ⊆ x4.
Assume H7:
and (equip x0 x6) (∀ x7 . x7 ∈ x6 ⟶ ∀ x8 . x8 ∈ x6 ⟶ (x7 = x8 ⟶ ∀ x9 : ο . x9) ⟶ x5 x7 x8).
Apply H7 with
or (∃ x7 . and (x7 ⊆ x4) (and (atleastp x1 x7) (∀ x8 . ... ⟶ ∀ x9 . ... ⟶ ... ⟶ x5 x8 ...))) ....