Let x0 of type ι be given.
Let x1 of type ι → ο be given.
Apply unknownprop_dec2978c0a72cebd51fcab0a380f03d4d80d1ccd8f826d378953148c305a60f0 with
4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))),
x0,
x1 x0 leaving 3 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_188fa0b3be5bd00c8929de7ba4788ef020b466ed1dea62f5d969ffccf9b84f3c with
x0,
x1 leaving 8 subgoals.
The subproof is completed by applying H9.
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.
The subproof is completed by applying H7.
Apply H9 with
λ x2 x3 . x1 x3.
The subproof is completed by applying H8.