Let x0 of type ο be given.
Let x1 of type ο be given.
Let x2 of type ο be given.
Assume H1: x1.
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_dc56e861c575e4f8f2a5658d6506d382dda41d92f4951b6eaf41874bb1aceaa9 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.