Let x0 of type ο be given.
Let x1 of type ο be given.
Let x2 of type ο be given.
Assume H0: x0.
Apply unknownprop_6c693c6a2aae4a815ab9dda6ac030d427fa2267caf48088e8c9791aaf5b51416 with
λ x3 x4 : ο → ο → ο → ο . x4 x0 x1 x2.
Apply unknownprop_7c688f24c3595bc4b513e911d7f551c8ccfedc804a6c15c02d25d01a2996aec6 with
and (exactly1of2 x0 x1) (not x2),
and (and (not x0) (not x1)) x2.
Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with
exactly1of2 x0 x1,
not x2 leaving 2 subgoals.
Apply unknownprop_220b0555ae9a3bd80693d86a463e0238690c5406559b0ede0f7a5dec827ff574 with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.