proposition: Lemma Prop_join_shrink: forall {U} (A B C R: Ensemble U), Included B R -> Prop_join A B C -> Prop_join (Intersection _ A R) B (Intersection _ C R).
proof: Proof. unfold Prop_join, Included, Ensembles.In. intros. split; intros; rewrite !Intersection_spec in *; auto. + split; firstorder. + firstorder. Qed.
imports: Coq.Classes.Morphisms Coq.Classes.Equivalence Coq.Sets.Ensembles Coq.Sets.Constructive_sets CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext