proposition: Lemma Ensemble_join_Intersection_Complement: forall {A} P Q, Included Q P -> (forall x, Q x \/ ~ Q x) -> Prop_join Q (Intersection A P (Complement A Q)) P.
proof: Proof. intros. unfold Prop_join. unfold Included, Ensembles.In in H. split; intros x; specialize (H0 x); specialize (H x); rewrite Intersection_spec; unfold Complement, Ensembles.In; try tauto. Qed.
imports: Coq.Classes.Morphisms Coq.Classes.Equivalence Coq.Sets.Ensembles Coq.Sets.Constructive_sets CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext