proposition: Lemma comp_is_id_then_injective : forall (A B : Setoid) (f : MAP A B) (g : MAP B A), Equal (comp_map_map g f) (Id A) -> injective f.
proof: Proof. intros A B f g H'; try assumption. apply comp_injective with A g; auto with algebra. apply injective_comp with (f := Id A); auto with algebra. Qed.