Apply unknownprop_72dc8a048701bf51fd7b8ba6b7bf88eb6b499e1dce5a6cc41194ad4cd8a8616a with
λ x0 . λ x1 : ι → ο . ∀ x2 : ο . (x0 = 5e331.. ⟶ x1 = 07017.. ⟶ x2) ⟶ (∀ x3 x4 . ∀ x5 x6 : ι → ο . 858ff.. x3 x5 ⟶ 858ff.. x4 x6 ⟶ x0 = a3eb9.. x3 x4 ⟶ x1 = c0709.. x5 x6 ⟶ x2) ⟶ (∀ x3 x4 . ∀ x5 x6 : ι → ο . 858ff.. x3 x5 ⟶ 858ff.. x4 x6 ⟶ x0 = bf68c.. x3 x4 ⟶ x1 = 6e020.. x5 x6 ⟶ x2) ⟶ x2 leaving 3 subgoals.
Let x0 of type ο be given.
Apply H0 leaving 2 subgoals.
Let x1 of type ι → ι → ο be given.
The subproof is completed by applying H3.
Let x1 of type (ι → ο) → (ι → ο) → ο be given.
The subproof is completed by applying H3.
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.