Apply unknownprop_0fbe0fac1c953bb3c5439340bfe4154388fda932cdbff43ad91d952f7a9846b8 with
False.
Let x0 of type ι → ι → ο be given.
Assume H1:
(λ x1 : ι → ι → ο . ∀ x2 : ο . ((∀ x3 x4 . x1 x3 x4 ⟶ x1 x4 x3) ⟶ x1 0 1 ⟶ x1 1 2 ⟶ x1 2 3 ⟶ x1 3 4 ⟶ x1 4 0 ⟶ not (x1 0 2) ⟶ not (x1 0 3) ⟶ not (x1 1 3) ⟶ not (x1 1 4) ⟶ not (x1 2 4) ⟶ x2) ⟶ x2) x0.
Apply H1 with
False.
Assume H2: ∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1.
Assume H3: x0 0 1.
Assume H4: x0 1 2.
Assume H5: x0 2 3.
Assume H6: x0 3 4.
Assume H7: x0 4 0.
Assume H10:
not (x0 1 3).
Assume H11:
not (x0 1 4).
Assume H12:
not (x0 2 4).
Apply H0 with
x0,
False leaving 3 subgoals.
The subproof is completed by applying H2.
Assume H14:
∃ x1 . and (x1 ⊆ 5) (and (equip 3 x1) (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3)).
Apply H14 with
False.
Let x1 of type ι be given.
Assume H15:
(λ x2 . and (x2 ⊆ 5) (and (equip 3 x2) (∀ x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ∈ x2 ⟶ (x3 = x4 ⟶ ∀ x5 : ο . x5) ⟶ x0 x3 x4))) x1.
Apply H15 with
False.
Assume H16: x1 ⊆ 5.
Assume H17:
and (equip 3 x1) (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3).
Apply H17 with
False.
Assume H19: ∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3.
Apply L13 with
x1,
False leaving 3 subgoals.
The subproof is completed by applying H16.
The subproof is completed by applying H18.
Assume H20:
∃ x2 . and (x2 ∈ x1) (∃ x3 . and (x3 ∈ x1) (and (x2 = x3 ⟶ ∀ x4 : ο . x4) (x0 x2 x3))).
Assume H21:
∃ x2 . and (x2 ∈ x1) (∃ x3 . and (x3 ∈ x1) (and (x2 = x3 ⟶ ∀ x4 : ο . x4) (not (x0 x2 x3)))).
Apply H21 with
False.
Let x2 of type ι be given.
Assume H22:
(λ x3 . and (x3 ∈ x1) (∃ x4 . and (x4 ∈ x1) (and (x3 = ... ⟶ ∀ x5 : ο . x5) ...))) ....