Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι → ο be given.
Let x3 of type ι → ο be given.
Assume H2:
PNoLe x0 x2 x1 x3.
Assume H3:
PNoLe x1 x3 x0 x2.
Apply unknownprop_a0b9870a33f18f7eb5aaf7ae107d529d6499166437a3535589b34653050e816a with
x0,
x1,
x2,
x3,
and (x0 = x1) (PNoEq_ x0 x2 x3) leaving 3 subgoals.
The subproof is completed by applying H2.
Assume H4:
PNoLt x0 x2 x1 x3.
Apply FalseE with
and (x0 = x1) (PNoEq_ x0 x2 x3).
Apply unknownprop_a0b9870a33f18f7eb5aaf7ae107d529d6499166437a3535589b34653050e816a with
x1,
x0,
x3,
x2,
False leaving 3 subgoals.
The subproof is completed by applying H3.
Assume H5:
PNoLt x1 x3 x0 x2.
Apply unknownprop_538b32da6e929848b1738bc95c54e7b85ed02786c342b641da55ecd1e295e69b with
x0,
x2.
Apply unknownprop_6bb26b25b4b138d2d5816191bcd658afb4958cf8c28d95f1e213b943c7319173 with
x0,
x1,
x0,
x2,
x3,
x2 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
Assume H5: x1 = x0.
Apply unknownprop_ee0b4b64aba8e6af97035d72b359ab8e1ae1e5e06024c58477c9410cad648356 with
λ x4 x5 : ι → (ι → ο) → (ι → ο) → ο . x5 x1 x3 x2 ⟶ False.
Assume H6:
(λ x4 . λ x5 x6 : ι → ο . ∀ x7 . In x7 x4 ⟶ iff (x5 x7) (x6 x7)) x1 x3 x2.
Apply unknownprop_7d798c5794ed96c61cc9ec828963a5831eee43021e8f1ea48be05a5cb53904e0 with
x0,
x1,
x2,
x3,
False leaving 4 subgoals.
The subproof is completed by applying H4.
Apply unknownprop_ff2db5d7cd089ead6d3f23ab1904a643f023d611ddbe42c5c85e87e080e26158 with
binintersect x0 x1,
x2,
x3,
False leaving 2 subgoals.
The subproof is completed by applying H7.
Let x4 of type ι be given.
Apply unknownprop_9f9c1680d203bdbb862d1bf6c2b8504d7e3a6fca72f77bd8968e86ad6ad69346 with
x0,
x1,
x4,
PNoEq_ x4 x2 x3 ⟶ not (x2 x4) ⟶ x3 x4 ⟶ False leaving 2 subgoals.
The subproof is completed by applying H8.
Assume H13: x3 x4.
Apply notE with
x2 x4 leaving 2 subgoals.
The subproof is completed by applying H12.
Apply unknownprop_d4c6f9663742385071dd283da85a9397dc2dfd0eede50c9fd289b7b23ca97cdd with
x3 x4,
x2 x4 leaving 2 subgoals.
Apply H6 with
x4.
The subproof is completed by applying H10.
The subproof is completed by applying H13.
Assume H9: x3 x0.
Apply unknownprop_60a0545f75dffa8edcef0ebd95f0c8e1071ecdfa5679c45641fd22ee51a570c9 with
x0.
Apply H5 with
λ x4 x5 . In x0 x4.
The subproof is completed by applying H7.
Apply unknownprop_60a0545f75dffa8edcef0ebd95f0c8e1071ecdfa5679c45641fd22ee51a570c9 with
x0.
Apply H5 with
λ x4 x5 . In x4 x0.
The subproof is completed by applying H7.
Assume H4: x0 = x1.
Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with
x0 = x1,
PNoEq_ x0 x2 x3 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H5.