proposition: Lemma EnvironStable_var_relation_closed: forall S (P: environ -> mpred), EnvironStable (vars_relation S) P <-> closed_wrt_vars S P.
proof: Proof. intros. unfold EnvironStable, vars_relation, closed_wrt_vars. split. + intros. specialize (H rho (mkEnviron (ge_of rho) (ve_of rho) te')). apply H. split; eauto. + intros. destruct H0 as [? [? ?]]. subst rho'. apply H; auto. Qed.
imports: CertiGraph.lib.Equivalence_ext CertiGraph.veric_ext.SeparationLogic VST.floyd.base VST.floyd.client_lemmas VST.floyd.assert_lemmas VST.floyd.closed_lemmas VST.floyd.forward_lemmas