Apply unknownprop_abe15cc9bd131c95b0b9585b43caa22ca6fcee57a092fd0cd1b55cd95e75595e with
λ x0 x1 : ι → ι → ι . ∀ x2 . ∀ x3 : ι → ι . ∀ x4 . In x4 (lam x2 (λ x5 . x3 x5)) ⟶ ∃ x5 . and (In x5 x2) (∃ x6 . and (In x6 (x3 x5)) (x4 = x0 x5 x6)).
The subproof is completed by applying unknownprop_f25818182af6b093121a8b5d43847162c8ea91396e524cca02557613a430a57a.