Let x0 of type ι be given.
Let x1 of type ι → ο be given.
Apply unknownprop_e284d5f5a7c3a1c03631041619c4ddee06de72330506f5f6d9d6b18df929e48c with
PNoLt x0 x1 x0 x1.
Assume H0:
PNoLt x0 x1 x0 x1.
Apply unknownprop_7d798c5794ed96c61cc9ec828963a5831eee43021e8f1ea48be05a5cb53904e0 with
x0,
x0,
x1,
x1,
False leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying unknownprop_76614fa912ebf79ea0c29bc2fb1b8d52bbbeb1883f999286b8533b64beff627a with
binintersect x0 x0,
x1.
Apply FalseE with
PNoEq_ x0 x1 x1 ⟶ x1 x0 ⟶ False.
Apply unknownprop_60a0545f75dffa8edcef0ebd95f0c8e1071ecdfa5679c45641fd22ee51a570c9 with
x0.
The subproof is completed by applying H1.
Apply FalseE with
PNoEq_ x0 x1 x1 ⟶ not (x1 x0) ⟶ False.
Apply unknownprop_60a0545f75dffa8edcef0ebd95f0c8e1071ecdfa5679c45641fd22ee51a570c9 with
x0.
The subproof is completed by applying H1.