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:
∀ x4 . In x4 x0 ⟶ In x2 (x1 x4) ⟶ x3.
Apply unknownprop_6aa6a1e2972a64fa9285a0890d0ac4772ddcd8c250de1b168f8abb7d1edde683 with
x0,
x1,
x2,
x3 leaving 2 subgoals.
The subproof is completed by applying H0.
Let x4 of type ι be given.
Assume H2:
(λ x5 . and (In x5 x0) (In x2 (x1 x5))) x4.
Apply andE with
In x4 x0,
In x2 (x1 x4),
x3 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H1 with x4.