Let x0 of type ο be given.
Let x1 of type ο be given.
Apply unknownprop_205dfda454738bda674e818ce60f3fddbf0921edb32095af6ffb25f2a0bd5888 with
λ x2 x3 : ο → ο → ο . not (x3 x0 x1) ⟶ (x0 ⟶ x1 ⟶ False) ⟶ (not x0 ⟶ not x1 ⟶ False) ⟶ False.
Assume H1:
x0 ⟶ x1 ⟶ False.
Apply unknownprop_f85aa429acea90bb5debe460a66fa5f521ae89262b26067dee6e29fd96c2cb64 with
and x0 (not x1),
and (not x0) x1 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_5aa3e99525b633063b3bdf7de851f763cb73cb264458fc7777fd7e7d458d63b5 with
x0,
not x1 leaving 3 subgoals.
The subproof is completed by applying H3.
Apply unknownprop_5aa3e99525b633063b3bdf7de851f763cb73cb264458fc7777fd7e7d458d63b5 with
not x0,
x1 leaving 3 subgoals.
The subproof is completed by applying H4.
Apply notE with
not x0 leaving 2 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying H5.
Apply H2 leaving 2 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H6.
Apply unknownprop_5aa3e99525b633063b3bdf7de851f763cb73cb264458fc7777fd7e7d458d63b5 with
not x0,
x1 leaving 3 subgoals.
The subproof is completed by applying H4.
Apply H1 leaving 2 subgoals.
Apply unknownprop_1e0cb2b8ae8b2a70437458035764f08e7eaba30fc84a0048f28b1466366514c4 with
x0.
The subproof is completed by applying H6.
Apply unknownprop_1e0cb2b8ae8b2a70437458035764f08e7eaba30fc84a0048f28b1466366514c4 with
x1.
The subproof is completed by applying H5.
Apply notE with
not x1 leaving 2 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H6.