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 ⟶ ∀ x5 : ο . (x0 ⟶ not x1 ⟶ not x2 ⟶ x5) ⟶ (not x0 ⟶ x1 ⟶ not x2 ⟶ x5) ⟶ (not x0 ⟶ not x1 ⟶ x2 ⟶ x5) ⟶ x5.
Let x3 of type ο be given.
Assume H1:
x0 ⟶ not x1 ⟶ not x2 ⟶ x3.
Assume H2:
not x0 ⟶ x1 ⟶ not x2 ⟶ x3.
Assume H3:
not x0 ⟶ not x1 ⟶ x2 ⟶ x3.
Apply unknownprop_eb8e8f72a91f1b934993d4cb19c84c8270f73a3626f3022b683d960a7fef89cb with
and (exactly1of2 x0 x1) (not x2),
and (and (not x0) (not x1)) x2,
x3 leaving 3 subgoals.
The subproof is completed by applying H0.
Apply andE with
exactly1of2 x0 x1,
not x2,
x3 leaving 2 subgoals.
The subproof is completed by applying H4.
Apply unknownprop_22b63889168c3c27321f1d9d99a6c13d916b48d833ad1ef7079baee20e0a05c6 with
x0,
x1,
x3 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_1eb28f5831a9d21e218b89c238edbbf849d22045bb77ce7cec926a651d1793f0 with
not x0,
not x1,
x2,
x3 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H3.