Let A, Y and c be given.

Assume HcY: c ∈ Y.

Let x and y be given.

Assume Hxy: (x,y) ∈ {(a,c)|a ∈ A}.

We will prove y ∈ Y.

Apply (ReplE_impred A (λa0 : set ⇒ (a0,c)) (x,y) Hxy (y ∈ Y)) to the current goal.

Let a be given.

Assume Ha: a ∈ A.

Assume Heq: (x,y) = (a,c).

We prove the intermediate claim Hyc: y = c.

rewrite the current goal using (tuple_2_1_eq x y) (from right to left).

rewrite the current goal using (tuple_2_1_eq a c) (from right to left).

rewrite the current goal using Heq (from left to right).

Use reflexivity.

rewrite the current goal using Hyc (from left to right).

An exact proof term for the current goal is HcY.

∎