Let p be given.
Assume HpRR: p ∈ setprod R R.
We will prove apply_fun add_fun_R p ∈ R.
We prove the intermediate claim Hp0R: p 0 ∈ R.
An exact proof term for the current goal is (ap0_Sigma R (λ_ : set ⇒ R) p HpRR).
We prove the intermediate claim Hp1R: p 1 ∈ R.
An exact proof term for the current goal is (ap1_Sigma R (λ_ : set ⇒ R) p HpRR).
We prove the intermediate claim Hdef: add_fun_R = graph (setprod R R) (λp0 : set ⇒ add_SNo (p0 0) (p0 1)).
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
rewrite the current goal using (apply_fun_graph (setprod R R) (λp0 : set ⇒ add_SNo (p0 0) (p0 1)) p HpRR) (from left to right).
An exact proof term for the current goal is (real_add_SNo (p 0) Hp0R (p 1) Hp1R).
∎