Apply unknownprop_abe15cc9bd131c95b0b9585b43caa22ca6fcee57a092fd0cd1b55cd95e75595e with
λ x0 x1 : ι → ι → ι . ∀ x2 . ∀ x3 : ι → ι . ∀ x4 . In x4 (lam x2 (λ x5 . x3 x5)) ⟶ x0 (ap x4 0) (ap x4 1) = x4.
The subproof is completed by applying unknownprop_c6f0b3e43ba2e277bdb674e47c0f34c61fb4e19c8f2afe3829a93549e478ca44.