Let x0 of type ο be given.
Let x1 of type ο be given.
Assume H0:
not (x0 = x1).
Assume H1: x1 ⟶ x0.
Apply unknownprop_e284d5f5a7c3a1c03631041619c4ddee06de72330506f5f6d9d6b18df929e48c with
x0 ⟶ x1.
Assume H2: x0 ⟶ x1.
Apply notE with
not (x0 = x1) leaving 2 subgoals.
set y2 to be x0 = x1
Claim L3: y2
set y3 to be λ x3 : ο → ο → ο . ∀ x4 x5 : ο . x3 x4 x5 ⟶ x4 = x5
Apply unknownprop_535a42de1055bca61f176bc11115db76b3356ad18505799408acb5bdbd2addc1 with
λ x4 x5 : ο → ο → ο . y3 x4,
y2,
y3 leaving 2 subgoals.
The subproof is completed by applying unknownprop_b721f4f18dab854a9c2f0364e7fd5ead1b477fed2e73a22ec4a16267b9cc37cb.
Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with
y2 ⟶ y3,
y3 ⟶ y2 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H1.
Apply unknownprop_e284d5f5a7c3a1c03631041619c4ddee06de72330506f5f6d9d6b18df929e48c with
not y2.
Apply notE with
y2 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying L3.
The subproof is completed by applying H0.