proposition: Lemma Included_Disjoint: forall A P Q P' Q', Included P P' -> Included Q Q' -> Disjoint A P' Q' -> Disjoint A P Q.
proof: Proof. intros. rewrite Disjoint_spec in H1 |- *. intros; apply (H1 x). + apply H; auto. + apply H0; auto. Qed.
imports: Coq.Classes.Morphisms Coq.Classes.Equivalence Coq.Sets.Ensembles Coq.Sets.Constructive_sets CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext