Let A, x, a and y be given.

Assume H: (a,y) ∈ const_fun A x.

We will prove y = x.

Apply (ReplE_impred A (λa0 : set ⇒ (a0,x)) (a,y) H (y = x)) to the current goal.

Let a0 be given.

Assume _: a0 ∈ A.

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

An exact proof term for the current goal is (tuple_2_1_congr a y a0 x Heq).

∎