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.
Let x6 of type ι → ι → ο be given.
Assume H4: ∀ x7 x8 . x6 x7 x8 ⟶ x6 x8 x7.
Apply H2 with
or (∃ x7 . and (x7 ⊆ x5) (and (equip x3 x7) (∀ x8 . x8 ∈ x7 ⟶ ∀ x9 . x9 ∈ x7 ⟶ (x8 = x9 ⟶ ∀ x10 : ο . x10) ⟶ x6 x8 x9))) (∃ x7 . and (x7 ⊆ x5) (and (equip x4 x7) (∀ x8 . x8 ∈ x7 ⟶ ∀ x9 . x9 ∈ x7 ⟶ (x8 = x9 ⟶ ∀ x10 : ο . x10) ⟶ not (x6 x8 x9)))).
Let x7 of type ι → ι be given.
Apply H3 with
λ x8 x9 . x6 (x7 x8) (x7 x9),
or (∃ x8 . and (x8 ⊆ x5) (and (equip x3 x8) (∀ x9 . x9 ∈ x8 ⟶ ∀ x10 . x10 ∈ x8 ⟶ (x9 = x10 ⟶ ∀ x11 : ο . x11) ⟶ x6 x9 x10))) (∃ x8 . and (x8 ⊆ x5) (and (equip x4 x8) (∀ x9 . x9 ∈ x8 ⟶ ∀ x10 . x10 ∈ x8 ⟶ (x9 = x10 ⟶ ∀ x11 : ο . x11) ⟶ not (x6 x9 x10)))) leaving 3 subgoals.
The subproof is completed by applying L6.
Assume H7:
∃ x8 . and (x8 ⊆ x2) (and (equip x0 x8) (∀ x9 . x9 ∈ x8 ⟶ ∀ x10 . x10 ∈ x8 ⟶ (x9 = x10 ⟶ ∀ x11 : ο . x11) ⟶ (λ x11 x12 . x6 (x7 x11) (x7 x12)) x9 x10)).
Apply orIL with
∃ x8 . and (x8 ⊆ x5) (and (equip x3 x8) (∀ x9 . x9 ∈ x8 ⟶ ∀ x10 . x10 ∈ x8 ⟶ (x9 = x10 ⟶ ∀ x11 : ο . x11) ⟶ x6 x9 x10)),
∃ x8 . and (x8 ⊆ x5) (and (equip x4 x8) (∀ x9 . x9 ∈ x8 ⟶ ∀ x10 . x10 ∈ x8 ⟶ (x9 = x10 ⟶ ∀ x11 : ο . x11) ⟶ not (x6 x9 x10))).
Apply unknownprop_a573fcf5678da4095e6e3bf5046c3135bfe4188e3dfb53e0dc34f5c73e140904 with
x0,
x3,
x2,
x5,
x6,
x7 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H5.
The subproof is completed by applying H7.
Assume H7:
∃ x8 . and (x8 ⊆ x2) (and (equip x1 x8) (∀ x9 . x9 ∈ x8 ⟶ ∀ x10 . x10 ∈ x8 ⟶ (x9 = x10 ⟶ ∀ x11 : ο . x11) ⟶ not ((λ x11 x12 . x6 (x7 x11) (x7 x12)) x9 x10))).
Apply orIR with
∃ x8 . and (x8 ⊆ x5) (and (equip x3 ...) ...),
....