proposition: Lemma guarded_surj_Disjoint: forall {X Y} (f: X -> Y) (PX: X -> Prop) (PY PY0: Y -> Prop), (forall y, PY y -> exists x, PX x /\ f x = y) -> (forall x, PX x -> ~ PY0 (f x)) -> Disjoint Y PY PY0.
proof: Proof. intros. rewrite Disjoint_spec. intros y ? ?. destruct (H _ H1) as [x [? ?]]. subst y. apply (H0 x); auto. Qed.
imports: Coq.Relations.Relation_Definitions Coq.Classes.Morphisms CertiGraph.lib.Coqlib CertiGraph.lib.Ensembles_ext CertiGraph.lib.Relation_ext CertiGraph.lib.Equivalence_ext CertiGraph.lib.EquivDec_ext