fact: Definition vars_relation (S: ident -> Prop) (rho rho': environ) : Prop := (forall i : ident, S i \/ Map.get (te_of rho) i = Map.get (te_of rho') i) /\ (exists te', rho' = mkEnviron (ge_of rho) (ve_of rho) te').
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