Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι → ι be given.
Assume H0:
∀ x3 . In x3 x0 ⟶ In (x2 x3) x1.
Apply unknownprop_9579ad195736876dd5df05c987aa079a6bacb25bc99006ef7b42c5a972f244df with
x0,
x1,
lam x0 (λ x3 . x2 x3).
Apply unknownprop_ae7ff6762664969563026849f911ad347655d2dee93f3e04751eb40cfcd41ed9 with
x0,
λ x3 . x1,
x2.
The subproof is completed by applying H0.