proposition: Lemma resp_Intersection: forall {A B: Type} (X Y: Ensemble B) (f: A -> B), Same_set (respectful_set (Intersection _ X Y) f) (Intersection _ (respectful_set X f) (respectful_set Y f)).
proof: Proof. intros. rewrite Same_set_spec; intros x. unfold respectful_set. rewrite !Intersection_spec. reflexivity. Qed.
imports: Coq.Classes.Morphisms Coq.Classes.Equivalence Coq.Sets.Ensembles Coq.Sets.Constructive_sets CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext