Let X, Y and p be given.
Assume Hp: p ∈ setprod X Y.
We will prove apply_fun (projection1 X Y) p = p 0.
We will prove Eps_i (λz ⇒ (p,z) ∈ projection1 X Y) = p 0.
We prove the intermediate claim H1: (p,p 0) ∈ projection1 X Y.
An exact proof term for the current goal is (ReplI (setprod X Y) (λq : set ⇒ (q,q 0)) p Hp).
We prove the intermediate claim H2: (p,Eps_i (λz ⇒ (p,z) ∈ projection1 X Y)) ∈ projection1 X Y.
An exact proof term for the current goal is (Eps_i_ax (λz ⇒ (p,z) ∈ projection1 X Y) (p 0) H1).
Apply (ReplE_impred (setprod X Y) (λq : set ⇒ (q,q 0)) (p,Eps_i (λz ⇒ (p,z) ∈ projection1 X Y)) H2) to the current goal.
Let q be given.
Assume Hq: q ∈ setprod X Y.
Assume Heq: (p,Eps_i (λz ⇒ (p,z) ∈ projection1 X Y)) = (q,q 0).
We prove the intermediate claim Hpq: p = q.
rewrite the current goal using (tuple_2_0_eq p (Eps_i (λz ⇒ (p,z) ∈ projection1 X Y))) (from right to left).
rewrite the current goal using (tuple_2_0_eq q (q 0)) (from right to left).
rewrite the current goal using Heq (from left to right).
Use reflexivity.
We prove the intermediate claim Hzq0: Eps_i (λz ⇒ (p,z) ∈ projection1 X Y) = q 0.
rewrite the current goal using (tuple_2_1_eq p (Eps_i (λz ⇒ (p,z) ∈ projection1 X Y))) (from right to left).
rewrite the current goal using (tuple_2_1_eq q (q 0)) (from right to left).
rewrite the current goal using Heq (from left to right).
Use reflexivity.
We prove the intermediate claim Hq0p0: q 0 = p 0.
rewrite the current goal using Hpq (from right to left).
Use reflexivity.
rewrite the current goal using Hzq0 (from left to right).
An exact proof term for the current goal is Hq0p0.
∎