proposition: Lemma Prop_join_shrink1: forall {U} (A B C: Ensemble U) (x: U), A x -> Prop_join A B C -> Prop_join (Intersection _ A (fun x0 => x <> x0)) B (Intersection _ C (fun x0 => x <> x0)).
proof: Proof. intros. apply Prop_join_shrink; auto. unfold Included, In; intros. intro. subst x0. destruct H0. apply (H2 x); auto. Qed.
imports: Coq.Classes.Morphisms Coq.Classes.Equivalence Coq.Sets.Ensembles Coq.Sets.Constructive_sets CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext