Let x0 of type ι be given.
Let x1 of type ι → ο be given.
Apply unknownprop_dec2978c0a72cebd51fcab0a380f03d4d80d1ccd8f826d378953148c305a60f0 with
4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))),
x0,
x1 x0 leaving 3 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_765cd5823a5c216bd034af6afe5edd62e0389ee8ea612a08b2cd6c866a00956d with
x0,
x1 leaving 7 subgoals.
The subproof is completed by applying H8.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
The subproof is completed by applying H6.
Apply H8 with
λ x2 x3 . x1 x3.
The subproof is completed by applying H7.