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