Let t be given.
Assume HtR: t ∈ R.
We will prove apply_fun neg_fun t = minus_SNo t.
We prove the intermediate claim Hdef: neg_fun = graph R (λt0 : set ⇒ minus_SNo t0).
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
rewrite the current goal using (apply_fun_graph R (λt0 : set ⇒ minus_SNo t0) t HtR) (from left to right).
Use reflexivity.
∎