Let x0 of type ι → (ι → ο) → ο be given.
Let x1 of type ι → (ι → ο) → ο be given.
Let x2 of type ι be given.
Let x3 of type ι → ο be given.
Let x4 of type ι → ο be given.
Apply H2 with
47618.. x0 x1 x2 x4.
Apply andI with
cae4c.. x0 x2 x4,
bc2b0.. x1 x2 x4 leaving 2 subgoals.
Apply unknownprop_601e47e4d78cdf42e2a3e2d8b99d86f42d29aff46b5fc48aae50649fe35bd708 with
x0,
x2,
x3,
x4 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
Apply unknownprop_e80a70fc28b36440a1efd4bd8be21f42fa8778462d8202d4a08b61486f7509ce with
x1,
x2,
x3,
x4 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H4.