proposition: Lemma is_guarded_inj_proper_aux1 {A B: Type} (P: A -> Prop) (f1 f2: A -> B): guarded_pointwise_relation P eq f1 f2 -> is_guarded_inj P f1 -> is_guarded_inj P f2.
proof: Proof. intros. destruct H0 as [g ?]. exists g. intro b; specialize (H0 b); destruct (g b). + destruct H0; split; auto. intros; specialize (H1 a0 H2). rewrite guarded_pointwise_relation_spec in H. rewrite H in H1 by auto; auto. + intros; specialize (H0 a H1). rewrite guarded_pointwise_relation_spec in H. rewrite H in H0 by auto; 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