proposition: Lemma semax_ram_seq_skip: forall Delta F P c Q, semax_ram Delta F P c Q <-> semax_ram Delta F P (Ssequence c Sskip) Q.
proof: Proof. intros. revert P Q; induction F; intros. + unfold semax_ram. apply semax_seq_skip. + destruct a; destruct real_frame; simpl. apply IHF. 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