proposition: Lemma is_guarded_inj_rev_aux' {A B: Type} (P1 P2: A -> Prop) (f: A -> B) (g1: B -> option A) (a: A): Disjoint B (image_set P1 f) (image_set P2 f) -> P2 a -> is_rev_fun P1 f g1 -> g1 (f a) = None.
proof: Proof. intros. specialize (H1 (f a)). destruct (g1 (f a)); auto. destruct H1. specialize (H2 a0 H1). pose proof proj2 H2 eq_refl. exfalso. rewrite Disjoint_spec in H. apply (H (f a0)). + constructor; auto. + rewrite H3; constructor; 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