proposition: Lemma guarded_pointwise_relation_weaken: forall {A B : Type} (P1 P2: A -> Prop) (R : relation B), Included P2 P1 -> inclusion _ (guarded_pointwise_relation P1 R) (guarded_pointwise_relation P2 R).
proof: Proof. intros. hnf; intros. rewrite guarded_pointwise_relation_spec in H0 |- *. unfold Included, In in H. firstorder. Qed.
imports: Coq.Relations.Relation_Definitions Coq.Classes.Morphisms CertiGraph.lib.Coqlib CertiGraph.lib.Ensembles_ext CertiGraph.lib.Relation_ext CertiGraph.lib.Equivalence_ext CertiGraph.lib.EquivDec_ext