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