proposition: Lemma ram_seq_assoc: forall Delta F P s1 s2 s3 R, semax_ram Delta F P (Ssequence s1 (Ssequence s2 s3)) R <-> semax_ram Delta F P (Ssequence (Ssequence s1 s2) s3) R.
proof: Proof. induction F; intros. + apply seq_assoc. + simpl. destruct a as [l g s [F0 ? ?]]. apply IHF; auto. 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