Let X, Y and p be given.
Assume Hp: p ∈ setprod X Y.
We will prove apply_fun (projection2 X Y) p = p 1.
We will prove Eps_i (λz ⇒ (p,z) ∈ projection2 X Y) = p 1.
We prove the intermediate claim H1: (p,p 1) ∈ projection2 X Y.
An exact proof term for the current goal is (ReplI (setprod X Y) (λq : set ⇒ (q,q 1)) p Hp).
We prove the intermediate claim H2: (p,Eps_i (λz ⇒ (p,z) ∈ projection2 X Y)) ∈ projection2 X Y.
An exact proof term for the current goal is (Eps_i_ax (λz ⇒ (p,z) ∈ projection2 X Y) (p 1) H1).
Apply (ReplE_impred (setprod X Y) (λq : set ⇒ (q,q 1)) (p,Eps_i (λz ⇒ (p,z) ∈ projection2 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) ∈ projection2 X Y)) = (q,q 1).
We prove the intermediate claim Hpq: p = q.
rewrite the current goal using (tuple_2_0_eq p (Eps_i (λz ⇒ (p,z) ∈ projection2 X Y))) (from right to left).
rewrite the current goal using (tuple_2_0_eq q (q 1)) (from right to left).
rewrite the current goal using Heq (from left to right).
Use reflexivity.
We prove the intermediate claim Hzq1: Eps_i (λz ⇒ (p,z) ∈ projection2 X Y) = q 1.
rewrite the current goal using (tuple_2_1_eq p (Eps_i (λz ⇒ (p,z) ∈ projection2 X Y))) (from right to left).
rewrite the current goal using (tuple_2_1_eq q (q 1)) (from right to left).
rewrite the current goal using Heq (from left to right).
Use reflexivity.
We prove the intermediate claim Hq1p1: q 1 = p 1.
rewrite the current goal using Hpq (from right to left).
Use reflexivity.
rewrite the current goal using Hzq1 (from left to right).
An exact proof term for the current goal is Hq1p1.
∎