Let A, f, g and a be given.
Assume Ha: a ∈ A.
Assume HfaR: apply_fun f a ∈ R.
Assume HgaR: apply_fun g a ∈ R.
We will prove apply_fun (compose_fun A (pair_map A f g) add_fun_R) a = add_SNo (apply_fun f a) (apply_fun g a).
rewrite the current goal using (compose_fun_apply A (pair_map A f g) add_fun_R a Ha) (from left to right).
rewrite the current goal using (pair_map_apply A R R f g a Ha) (from left to right) at position 1.
We prove the intermediate claim HpRR: (apply_fun f a,apply_fun g a) ∈ setprod R R.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R (apply_fun f a) (apply_fun g a) HfaR HgaR).
rewrite the current goal using (add_fun_R_apply (apply_fun f a,apply_fun g a) HpRR) (from left to right).
rewrite the current goal using (tuple_2_0_eq (apply_fun f a) (apply_fun g a)) (from left to right) at position 1.
rewrite the current goal using (tuple_2_1_eq (apply_fun f a) (apply_fun g a)) (from left to right) at position 1.
Use reflexivity.
∎