proposition: Lemma semax_ram_seq': forall Delta F F' P Q R c, add_stats c F F' -> semax Delta P c (normal_ret_assert Q) -> semax_ram (update_tycon Delta c) F' Q Sskip R -> semax_ram Delta F P c R.
proof: Proof. intros. rewrite semax_ram_seq_skip. eapply semax_ram_seq; eauto. Qed.
imports: CertiGraph.lib.Ensembles_ext CertiGraph.lib.Relation_ext CertiGraph.lib.List_ext CertiGraph.veric_ext.SeparationLogic CertiGraph.floyd_ext.ramification VST.floyd.base VST.floyd.canon VST.floyd.assert_lemmas VST.floyd.client_lemmas VST.floyd.closed_lemmas