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