proposition: Lemma cancelL_isinjective {A B C : Type} {f : A -> B} {g : B -> C} `{I : isinj (g o f)} : isinj f.
proof: Proof. intros a0 a1 p. apply I. exact (ap g p). Defined.
imports: Basics Types.Sigma Types.Forall Types.Paths Types.Unit Types.Arrow