Let x0 of type ι → (ι → ο) → ο be given.
Let x1 of type ι → (ι → ο) → ο be given.
Let x2 of type ι be given.
Apply unknownprop_6419f8fc1ff70ca950cf4e79a0f0cff9b9f9b876ea55c76aec20f2ed9adc5971 with
x0,
x1,
x2,
47618.. x0 x1 (7b9f3.. x0 x1) (ce2d5.. x0 x1) leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.