Let X, f, g and x be given.

Assume Hx.

We will prove Eps_i (λz ⇒ (x,z) ∈ {(y,apply_fun g (apply_fun f y))|y ∈ X}) = apply_fun g (apply_fun f x).

We prove the intermediate claim H1: (x,apply_fun g (apply_fun f x)) ∈ {(y,apply_fun g (apply_fun f y))|y ∈ X}.

An exact proof term for the current goal is (ReplI X (λy ⇒ (y,apply_fun g (apply_fun f y))) x Hx).

We prove the intermediate claim H2: (x,Eps_i (λz ⇒ (x,z) ∈ {(y,apply_fun g (apply_fun f y))|y ∈ X})) ∈ {(y,apply_fun g (apply_fun f y))|y ∈ X}.

An exact proof term for the current goal is (Eps_i_ax (λz ⇒ (x,z) ∈ {(y,apply_fun g (apply_fun f y))|y ∈ X}) (apply_fun g (apply_fun f x)) H1).

Apply (ReplE_impred X (λy ⇒ (y,apply_fun g (apply_fun f y))) (x,Eps_i (λz ⇒ (x,z) ∈ {(y,apply_fun g (apply_fun f y))|y ∈ X})) H2) to the current goal.

Let y be given.

Assume Hy: y ∈ X.

Assume Heq: (x,Eps_i (λz ⇒ (x,z) ∈ {(y0,apply_fun g (apply_fun f y0))|y0 ∈ X})) = (y,apply_fun g (apply_fun f y)).

We prove the intermediate claim Hx_eq: x = y.

rewrite the current goal using (tuple_2_0_eq x (Eps_i (λz ⇒ (x,z) ∈ {(y0,apply_fun g (apply_fun f y0))|y0 ∈ X}))) (from right to left).

rewrite the current goal using (tuple_2_0_eq y (apply_fun g (apply_fun f y))) (from right to left).

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

Use reflexivity.

We prove the intermediate claim Hz_eq: Eps_i (λz ⇒ (x,z) ∈ {(y0,apply_fun g (apply_fun f y0))|y0 ∈ X}) = apply_fun g (apply_fun f y).

rewrite the current goal using (tuple_2_1_eq x (Eps_i (λz ⇒ (x,z) ∈ {(y0,apply_fun g (apply_fun f y0))|y0 ∈ X}))) (from right to left).

rewrite the current goal using (tuple_2_1_eq y (apply_fun g (apply_fun f y))) (from right to left).

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

Use reflexivity.

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

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

Use reflexivity.

∎