Let x0 of type ι be given.
Let x1 of type ι → ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Apply unknownprop_dc1e02deebcd6c87d85e338d34fdf4caf44c0c3d3d8c7882c6574d39d68b0003 with
λ x4 x5 : ι → (ι → ι) → ι . In x2 (x5 x0 (λ x6 . x1 x6)) ⟶ In x3 x0 ⟶ In (ap x2 x3) (x1 x3).
Assume H0:
In x2 ((λ x4 . λ x5 : ι → ι . Sep (Power (lam x4 (λ x6 . Union (x5 x6)))) (λ x6 . ∀ x7 . In x7 x4 ⟶ In (ap x6 x7) (x5 x7))) x0 (λ x4 . x1 x4)).
Apply unknownprop_ba186f550679124419b8222be99b3e20dd42619ae850577f6f9edb2a83aac5a7 with
Power (lam x0 (λ x4 . Union (x1 x4))),
λ x4 . ∀ x5 . In x5 x0 ⟶ In (ap x4 x5) (x1 x5),
x2,
x3.
The subproof is completed by applying H0.