proposition: Lemma injective_comp : forall (A B : Setoid) (f f' : MAP A B), injective f -> Equal f f' -> injective f'.
proof: Proof. unfold injective in |- *. intros A B f f' H' H'0 x y H'1; try assumption. apply H'. apply Trans with (Ap f' x); auto with algebra. apply Trans with (Ap f' y); auto with algebra. Qed.