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