Let A, x, a and y be given.

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

We will prove a ∈ A.

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

Let a0 be given.

Assume Ha0: a0 ∈ A.

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

We prove the intermediate claim Ha: a = a0.

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

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

An exact proof term for the current goal is Ha0.

∎