proposition: Lemma comp_injective : forall (A B C : Setoid) (f : MAP A B) (g : MAP B C), injective (comp_map_map g f) -> injective f.
proof: Proof. unfold injective in |- *. intros A B C f g H' x y H'0; try assumption. apply H'. unfold comp_map_map in |- *; simpl in |- *. unfold comp_map_fun in |- *. auto with algebra. Qed.