Let x0 of type ο be given.
Let x1 of type ο be given.
Let x2 of type ο be given.
Apply unknownprop_6c693c6a2aae4a815ab9dda6ac030d427fa2267caf48088e8c9791aaf5b51416 with
λ x3 x4 : ο → ο → ο → ο . x4 x0 x1 x2 ⟶ (x0 ⟶ not x1 ⟶ not x2 ⟶ False) ⟶ (not x0 ⟶ x1 ⟶ not x2 ⟶ False) ⟶ (not x0 ⟶ not x1 ⟶ x2 ⟶ False) ⟶ False.
Apply unknownprop_29c71c3225679258502bd11dbc7045cf7d8f50eae8cff2bb65bd7e7026124a80 with
and (exactly1of2 x0 x1) (not x2),
and (and (not x0) (not x1)) x2 leaving 3 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_724993ddd07db7177fc4cfc8946faba70a46f419f0496c9045904e0954a499e1 with
exactly1of2 x0 x1,
not x2 leaving 2 subgoals.
The subproof is completed by applying H4.
Apply unknownprop_81cea01bd7c2d54cbff6ee24d81c85bb82ad2cbeddae1b920e3fc14b951b3e57 with
x0,
x1 leaving 3 subgoals.
The subproof is completed by applying H5.
Assume H7: x0.
Apply H1 leaving 3 subgoals.
The subproof is completed by applying H7.
The subproof is completed by applying H8.
The subproof is completed by applying H6.
Assume H8: x1.
Apply H2 leaving 3 subgoals.
The subproof is completed by applying H7.
The subproof is completed by applying H8.
The subproof is completed by applying H6.
Apply unknownprop_724993ddd07db7177fc4cfc8946faba70a46f419f0496c9045904e0954a499e1 with
and (not x0) (not x1),
x2 leaving 2 subgoals.
The subproof is completed by applying H4.
Assume H6: x2.
Apply unknownprop_724993ddd07db7177fc4cfc8946faba70a46f419f0496c9045904e0954a499e1 with
not x0,
not x1 leaving 2 subgoals.
The subproof is completed by applying H5.
Apply H3 leaving 3 subgoals.
The subproof is completed by applying H7.
The subproof is completed by applying H8.
The subproof is completed by applying H6.