Let A and g be given.

Let x, y1 and y2 be given.

Assume H1: (x,y1) ∈ {(a,g a)|a ∈ A}.

Assume H2: (x,y2) ∈ {(a,g a)|a ∈ A}.

Apply (ReplE_impred A (λa0 : set ⇒ (a0,g a0)) (x,y1) H1 (y1 = y2)) to the current goal.

Let a1 be given.

Assume Ha1: a1 ∈ A.

Assume Heq1: (x,y1) = (a1,g a1).

Apply (ReplE_impred A (λa0 : set ⇒ (a0,g a0)) (x,y2) H2 (y1 = y2)) to the current goal.

Let a2 be given.

Assume Ha2: a2 ∈ A.

Assume Heq2: (x,y2) = (a2,g a2).

We prove the intermediate claim Hx1: x = a1.

rewrite the current goal using (tuple_2_0_eq x y1) (from right to left).

rewrite the current goal using (tuple_2_0_eq a1 (g a1)) (from right to left).

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

Use reflexivity.

We prove the intermediate claim Hx2: x = a2.

rewrite the current goal using (tuple_2_0_eq x y2) (from right to left).

rewrite the current goal using (tuple_2_0_eq a2 (g a2)) (from right to left).

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

Use reflexivity.

We prove the intermediate claim Ha12: a1 = a2.

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

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

Use reflexivity.

We prove the intermediate claim Hy1: y1 = g a1.

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

rewrite the current goal using (tuple_2_1_eq a1 (g a1)) (from right to left).

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

Use reflexivity.

We prove the intermediate claim Hy2: y2 = g a2.

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

rewrite the current goal using (tuple_2_1_eq a2 (g a2)) (from right to left).

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

Use reflexivity.

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

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

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

Use reflexivity.

∎