proposition: Lemma vars_relation_Included: forall P Q, Included P Q -> inclusion _ (vars_relation P) (vars_relation Q).
proof: Proof. intros. intros ? ? ?. unfold vars_relation in *. split. + unfold Included, Ensembles.In in H. destruct H0 as [? _]. firstorder. + exact (proj2 H0). 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