Let A, x and a be given.
Assume Ha: a ∈ A.
We will prove apply_fun (const_fun A x) a = x.
We will prove Eps_i (λy ⇒ (a,y) ∈ const_fun A x) = x.
We prove the intermediate claim H1: (a,x) ∈ const_fun A x.
An exact proof term for the current goal is (ReplI A (λa0 : set ⇒ (a0,x)) a Ha).
We prove the intermediate claim H2: (a,Eps_i (λy ⇒ (a,y) ∈ const_fun A x)) ∈ const_fun A x.
An exact proof term for the current goal is (Eps_i_ax (λy ⇒ (a,y) ∈ const_fun A x) x H1).
Apply (ReplE_impred A (λa0 : set ⇒ (a0,x)) (a,Eps_i (λy ⇒ (a,y) ∈ const_fun A x)) H2) to the current goal.
Let a0 be given.
Assume Ha0: a0 ∈ A.
Assume Heq: (a,Eps_i (λy ⇒ (a,y) ∈ const_fun A x)) = (a0,x).
rewrite the current goal using (tuple_2_1_eq a (Eps_i (λy ⇒ (a,y) ∈ const_fun A x))) (from right to left) at position 1.
rewrite the current goal using (tuple_2_1_eq a0 x) (from right to left) at position 2.
rewrite the current goal using Heq (from left to right).
Use reflexivity.
∎