(f : A -> B) `{!IsInjective f} : IsStrongInjective f. Proof. split; try apply _. intros x y. intros ap. apply trivial_apart in ap. apply trivial_apart. intros e. apply ap. apply (injective f). assumption. Qed.
Require Import HoTT.Classes.interfaces.abstract_algebra.