Let c and t be given.

Assume HcR: c ∈ R.

Assume HtR: t ∈ R.

We prove the intermediate claim Hdef: div_const_fun c = graph R (λt0 : set ⇒ div_SNo t0 c).

Use reflexivity.

rewrite the current goal using Hdef (from left to right).

An exact proof term for the current goal is (apply_fun_graph R (λt0 : set ⇒ div_SNo t0 c) t HtR).

∎