proposition: Lemma is_guarded_inj_proper_aux2 {A B: Type} (P1 P2: A -> Prop) (f: A -> B): Same_set P1 P2 -> is_guarded_inj P1 f -> is_guarded_inj P2 f.
proof: Proof. intros. destruct H0 as [g ?]. exists g. rewrite Same_set_spec in H. intro b; specialize (H0 b); destruct (g b). + rewrite H in H0. destruct H0; split; auto. intros; rewrite <- H in H2; auto. + intros; rewrite <- H in H1; 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