Let X, P, F and y be given.

Assume H1: y ∈ {F x|x ∈ X, P x}.

Let p be given.

Assume H2: ∀x ∈ X, P x → y = F x → p.

We will prove p.

Apply ReplSepE X P F y H1 to the current goal.

Let x be given.

Assume H3.

Apply H3 to the current goal.

Assume H3.

Apply H3 to the current goal.

An exact proof term for the current goal is H2 x.

∎