proposition: Lemma ismono_isinj `{Funext} {X Y} (f : X -> Y) : isinj f -> ismono f.
proof: Proof. intros ? ? ? ? H'. apply path_forall. apply ap10 in H'. hnf in *. eauto. Qed.
imports: Basics Types.Sigma Types.Forall Types.Paths Types.Unit Types.Arrow