Let x0 of type ι be given.
Let x1 of type ι → ι be given.
Apply unknownprop_85c22e88a806aabda7246f27ac458442bcb94ac25cc9a3616a68cf646d95941d with
4ae4a.. 4a7ef..,
0fc90.. x0 (λ x2 . x1 x2).
Let x2 of type ι be given.
Apply and3E with
aae7a.. (e76d4.. x2) (22ca9.. x2) = x2,
prim1 (e76d4.. x2) x0,
prim1 (22ca9.. x2) (x1 (e76d4.. x2)),
x2 = 4a7ef.. leaving 2 subgoals.
Apply unknownprop_4861fab3b9bde4ccc5c91f323e4d2535c7d435027e9067e34ce3781cfa602d01 with
x0,
x1,
x2.
The subproof is completed by applying H2.
Apply unknownprop_30833a9978e304b25ffd59c347245315985872140acc9e441a97543a28184d79 with
4a7ef..,
e76d4.. x2.
Apply unknownprop_745f0ddae55929306ce167ef9bae0ede767961c0319e8b14305a55d5b24d73e4 with
e76d4.. x2.
Apply unknownprop_4134b8a5d866cd7ad711ea569ada0ca0ba949f5cad571bf5782dc7c2d15cdb1c with
4ae4a.. 4a7ef..,
x0,
e76d4.. x2 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H4.
Apply unknownprop_30833a9978e304b25ffd59c347245315985872140acc9e441a97543a28184d79 with
4a7ef..,
22ca9.. x2.
Apply unknownprop_745f0ddae55929306ce167ef9bae0ede767961c0319e8b14305a55d5b24d73e4 with
22ca9.. x2.
Apply unknownprop_4134b8a5d866cd7ad711ea569ada0ca0ba949f5cad571bf5782dc7c2d15cdb1c with
4ae4a.. 4a7ef..,
x1 (e76d4.. x2),
22ca9.. x2 leaving 2 subgoals.
Apply H1 with
e76d4.. x2.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
Apply H3 with
λ x3 x4 . x3 = 4a7ef...
Apply L6 with
λ x3 x4 . aae7a.. x4 (22ca9.. x2) = 4a7ef...
Apply L7 with
λ x3 x4 . aae7a.. 4a7ef.. x4 = 4a7ef...
The subproof is completed by applying unknownprop_1a54e7c6ffa26b28d1907d2422054a89d5f0b3d3f515023aed0bd83c9a97b0a8.
Apply L3 with
λ x3 x4 . prim1 x4 (4ae4a.. 4a7ef..).
The subproof is completed by applying unknownprop_375af585d676cd889234cd20860ce45033e1ffceb375ac6277c1b1a2e16f15bd.