Let x0 of type ο be given.
Let x1 of type ο be given.
Assume H0: x0 ⟶ x1.
Apply xm with
x0,
or (not x0) x1 leaving 2 subgoals.
Assume H1: x0.
Apply orIR with
not x0,
x1.
Apply H0.
The subproof is completed by applying H1.
Apply orIL with
not x0,
x1.
The subproof is completed by applying H1.