proposition: Lemma semax_ram_seq: forall Delta F F' P Q R c0 c1, add_stats c0 F F' -> semax Delta P c0 (normal_ret_assert Q) -> semax_ram (update_tycon Delta c0) F' Q c1 R -> semax_ram Delta F P (Ssequence c0 c1) R.
proof: Proof. intros. Opaque LiftNatDed' LiftSepLog'. revert P Q H0 H1; induction H; intros; simpl in H1 |- *. Transparent LiftNatDed' LiftSepLog'. + eapply semax_seq'; eauto. + eapply IHadd_stats; [| eauto]. rewrite <- frame_normal. apply semax_frame; auto. apply EnvironStable_var_relation_closed. apply EnvironBox_EnvironStable_weaken; [apply vars_relation_Equivalence |]. apply vars_relation_Included. hnf; unfold Ensembles.In, modifiedvars; simpl; intros. rewrite modifiedvars'_union in H2 |- *. rewrite (modifiedvars'_union _ c0). rewrite (modifiedvars'_union _ cont). tauto. 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