Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_4b95783dcb3eee1943e1de5542f675166ef402c8fbdda80bdf0920b55d3fc6de with
setexp 0 x0,
0,
λ x2 . x2.
Apply unknownprop_aa42ade5598d8612d2029318c4ed81646c550ecc6cdd9ab953ce4bf73f3dd562 with
setexp 0 x0,
0,
λ x2 . x2 leaving 2 subgoals.
Apply unknownprop_57c8600e4bc6abecef2ae17962906fa2de1fc16f5d46ed100ff99cd5b67f5b1b with
setexp 0 x0,
0,
λ x2 . x2 leaving 2 subgoals.
Let x2 of type ι be given.
Apply FalseE with
In ((λ x3 . x3) x2) 0.
Apply unknownprop_1cc88f7e87aaf8c5cee24b4a69ff535a81e7855c45a9fd971eec05ee4cc28f9c with
ap x2 x1.
Apply unknownprop_0850c5650a2b96b400e4741e4dbd234b5337d397bb9bfabc1463651d86151ddb with
x0,
0,
x2,
x1 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
Let x2 of type ι be given.
Apply FalseE with
∀ x3 . In x3 (setexp 0 x0) ⟶ (λ x4 . x4) x2 = (λ x4 . x4) x3 ⟶ x2 = x3.
Apply unknownprop_1cc88f7e87aaf8c5cee24b4a69ff535a81e7855c45a9fd971eec05ee4cc28f9c with
ap x2 x1.
Apply unknownprop_0850c5650a2b96b400e4741e4dbd234b5337d397bb9bfabc1463651d86151ddb with
x0,
0,
x2,
x1 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
Let x2 of type ι be given.
Apply FalseE with
∃ x3 . and (In x3 (setexp 0 x0)) ((λ x4 . x4) x3 = x2).
Apply unknownprop_1cc88f7e87aaf8c5cee24b4a69ff535a81e7855c45a9fd971eec05ee4cc28f9c with
x2.
The subproof is completed by applying H1.