proposition: Lemma injective_imp_injective_weak : forall A B (f : CSetoid_fun A B), injective f -> injective_weak f.
proof: Proof. intros A B f. unfold injective in |- *. intro H. unfold injective_weak in |- *. intros a0 a1 H0. apply not_ap_imp_eq. red in |- *. intro H1. set (H2 := H a0 a1 H1) in *. set (H3 := ap_imp_neq B (f a0) (f a1) H2) in *. set (H4 := eq_imp_not_neq B (f a0) (f a1) H0) in *. apply H4. exact H3. Qed.
imports: CoRN.algebra.CSetoids