{A B C : Type} (f : A -> B) (g : B -> C) `{!IsInjective (g o f)} : IsInjective f. Proof. intros x y p. apply (injective (g o f)). exact (ap g p). Defined.
Require Import Basics.Overture Basics.Tactics.