Let x0 of type ο be given.
Let x1 of type ο be given.
Assume H0: x0 ⟶ x1.
Apply unknownprop_658f94a759722b1602ef0d5fef336255c26508a4752d5563003b348e04f8cd54 with
not x0,
x1.
Apply notE with
x1 leaving 2 subgoals.
The subproof is completed by applying H2.
Apply H0.
Apply unknownprop_1e0cb2b8ae8b2a70437458035764f08e7eaba30fc84a0048f28b1466366514c4 with
x0.
The subproof is completed by applying H1.