rewrite the current goal using (apply_fun_graph A g a Ha) (from left to right).