Apply unknownprop_ca4ccf6887ff6dc7b05e5402a8b941f864c9703226396122edada9d3d18a208b with
λ x0 x1 : ι → (ι → ο) → (ι → ι) → ι . ∀ x2 . ∀ x3 : ι → ο . ∀ x4 : ι → ι . ∀ x5 . In x5 x2 ⟶ x3 x5 ⟶ In (x4 x5) (x1 x2 (λ x6 . x3 x6) (λ x6 . x4 x6)).
Let x0 of type ι be given.
Let x1 of type ι → ο be given.
Let x2 of type ι → ι be given.
Let x3 of type ι be given.
Assume H1: x1 x3.
Apply unknownprop_63c308b92260dbfca8c9530846e6836ba3e6be221cc8e80fd61db913e01bdacf with
Sep x0 x1,
x2,
x3.
Apply unknownprop_646b3add51cf8f8e84959b456822a93c7e59b2f394a14897b6752b9d28c1a75d with
x0,
x1,
x3 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.