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