Let x0 of type ο be given.
Apply FalseE.
Apply andE with
x0,
not True,
False leaving 2 subgoals.
The subproof is completed by applying H0.
Assume H1: x0.
Apply notE with
True leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying TrueI.