Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ο be given.
Apply unknownprop_1c12738cd89f8c615a541c15b6797bba2a5be97ab5e514c9fd76b3fef06e2aa9 with
e4431.. x0,
e4431.. x1,
λ x3 . prim1 x3 x0,
λ x3 . prim1 x3 x1,
x2 leaving 4 subgoals.
The subproof is completed by applying H2.
Apply PNoLt_E_ with
d3786.. (e4431.. x0) (e4431.. x1),
λ x3 . prim1 x3 x0,
λ x3 . prim1 x3 x1,
x2 leaving 2 subgoals.
The subproof is completed by applying H8.
Let x3 of type ι be given.
Apply unknownprop_1ac99d32a7ae5dc08fd640ea6c8b661df6b3535fe85e88b30b17c3701cb4c7ce with
e4431.. x0,
e4431.. x1,
x3,
x2 leaving 2 subgoals.
The subproof is completed by applying H9.
Apply unknownprop_2c27682abc32e1c8a2160a07043a81afe1f256df4f0472edf3cf11efdcea8609 with
09072.. x3 (λ x4 . prim1 x4 x0),
x2 leaving 2 subgoals.
The subproof is completed by applying L17.
Apply H3 with
09072.. x3 (λ x4 . prim1 x4 x0) leaving 8 subgoals.
The subproof is completed by applying L17.
Apply L20 with
λ x4 x5 . SNoEq_ x5 (09072.. x3 (λ x6 . prim1 x6 x0)) x0.
The subproof is completed by applying L21.
Apply L20 with
λ x4 x5 . SNoEq_ x5 (09072.. x3 (λ x6 . prim1 x6 x0)) x1.
The subproof is completed by applying L22.