Let f, A, g and a be given.

Assume Hf: f = graph A g.

Assume Ha: a ∈ A.

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

An exact proof term for the current goal is (apply_fun_graph A g a Ha).

∎