Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply unknownprop_fa66e3d1737b2c05fa4008399b4c740ee88bf9334c6b435957b41684dfedfe51 with
f482f.. (aae7a.. x0 x1) x2.
Let x3 of type ι be given.
Apply unknownprop_94a9448d53fe41e2f423017518d13b5ed4aaa7ee3f113a3a8a767ea0e11959dd with
aae7a.. x0 x1,
x2,
x3.
The subproof is completed by applying H1.
Apply unknownprop_583e189228469f510dae093aa816b0d084f1acaf0341e7deab9d9a676d1b11ef with
x0,
x1,
aae7a.. x2 x3,
False leaving 3 subgoals.
The subproof is completed by applying L2.
Apply exandE_i with
λ x4 . prim1 x4 x0,
λ x4 . aae7a.. x2 x3 = aae7a.. 4a7ef.. x4,
False leaving 2 subgoals.
The subproof is completed by applying H3.
Let x4 of type ι be given.
Apply unknownprop_25f0736e80681cd44329b5b6c9965a9cf95558c1b85c8430e91be63bfeb5cf39 with
x2,
x3,
4a7ef..,
x4,
False leaving 2 subgoals.
The subproof is completed by applying H5.
Assume H7: x3 = x4.
Apply H0.
Apply H6 with
λ x5 x6 . prim1 x6 (4ae4a.. (4ae4a.. 4a7ef..)).
The subproof is completed by applying unknownprop_94c438c3f41134cd86e0be06a85b5e5b3aa8448f9221f51d2dfe9b1364042f49.
Apply exandE_i with
λ x4 . prim1 x4 x1,
λ x4 . aae7a.. x2 x3 = aae7a.. (4ae4a.. 4a7ef..) x4,
False leaving 2 subgoals.
The subproof is completed by applying H3.
Let x4 of type ι be given.
Apply unknownprop_25f0736e80681cd44329b5b6c9965a9cf95558c1b85c8430e91be63bfeb5cf39 with
x2,
x3,
4ae4a.. 4a7ef..,
x4,
False leaving 2 subgoals.
The subproof is completed by applying H5.
Assume H7: x3 = x4.
Apply H0.
Apply H6 with
λ x5 x6 . prim1 x6 (4ae4a.. (4ae4a.. 4a7ef..)).
The subproof is completed by applying unknownprop_e256c3837ff221325e66d4c83283618d462d76cb96bca463e1abd4876bf63511.