Let X and x be given.
Assume Hx: x ∈ X.
We will prove apply_fun {(y,y)|y ∈ X} x = x.
We will prove Eps_i (λz ⇒ (x,z) ∈ {(y,y)|y ∈ X}) = x.
We prove the intermediate claim H1: (x,x) ∈ {(y,y)|y ∈ X}.
An exact proof term for the current goal is (ReplI X (λy ⇒ (y,y)) x Hx).
We prove the intermediate claim H2: (x,Eps_i (λz ⇒ (x,z) ∈ {(y,y)|y ∈ X})) ∈ {(y,y)|y ∈ X}.
An exact proof term for the current goal is (Eps_i_ax (λz ⇒ (x,z) ∈ {(y,y)|y ∈ X}) x H1).
Apply (ReplE_impred X (λy ⇒ (y,y)) (x,Eps_i (λz ⇒ (x,z) ∈ {(y,y)|y ∈ X})) H2) to the current goal.
Let y be given.
Assume Hy: y ∈ X.
Assume Heq: (x,Eps_i (λz ⇒ (x,z) ∈ {(y,y)|y ∈ X})) = (y,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) ∈ {(y,y)|y ∈ X}))) (from right to left).
rewrite the current goal using (tuple_2_0_eq y 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) ∈ {(y,y)|y ∈ X}) = y.
rewrite the current goal using (tuple_2_1_eq x (Eps_i (λz ⇒ (x,z) ∈ {(y,y)|y ∈ X}))) (from right to left).
rewrite the current goal using (tuple_2_1_eq y 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.
∎