Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_9cbe1b438cb309fdaf3dcacebb3b572a10a17828098a582be8e9441d5a1eab25 with
λ x2 x3 : ι → ι → ι . ∀ x4 . In x4 (x3 x1 x0) ⟶ lam x0 (λ x5 . ap x4 x5) = x4.
The subproof is completed by applying unknownprop_1d401bfd2bdb443cb4ed66a0412f4299139e285cca5e460f0f1c03467ae8078c with x0, λ x2 . x1.