proposition: Lemma body_forward: semax_body Vprog Gprog f_forward forward_spec.
proof: Proof. start_function. match goal with |- semax _ _ ?c _ => change c with (fn_body f_forward) end. change Delta with (func_tycontext f_forward Vprog Gprog nil). destruct forward_p. eapply body_forward_inL; eassumption. eapply body_forward_inR; eassumption. Qed.
imports: CertiGraph.CertiGC(env_graph_gc gc_spec) CertiGraph.msl_ext.ramification_lemmas CertiGraph.CertiGC.verif_forward1 CertiGraph.CertiGC.verif_forward2