Let x0 of type ι be given.
Let x1 of type ι → ο be given.
Let x2 of type ι → ι be given.
Let x3 of type ι be given.
Assume H0:
In x3 (ReplSep x0 (λ x4 . x1 x4) (λ x4 . x2 x4)).
Let x4 of type ο be given.
Assume H1:
∀ x5 . In x5 x0 ⟶ x1 x5 ⟶ x3 = x2 x5 ⟶ x4.
Apply unknownprop_3848cfb1fd522cb609408da39f227a9c05924a24919f21041d0880590b824ef5 with
λ x5 . and (In x5 x0) (x1 x5),
λ x5 . x3 = x2 x5,
x4 leaving 2 subgoals.
Apply unknownprop_b73fc33e023ecfdaf58582e4676cca683b73b9ba0baf712515ce501d3b01b224 with
x0,
x1,
x2,
x3.
The subproof is completed by applying H0.
Let x5 of type ι be given.
Assume H2:
and (In x5 x0) (x1 x5).
Apply andE with
In x5 x0,
x1 x5,
x3 = x2 x5 ⟶ x4 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H1 with x5.