proposition: Lemma monfunstnpr1_isInjective {m n} (f g : monfunstn m n) : monfunstnpr1 f = monfunstnpr1 g -> f = g.
proof: Proof. intros e. apply subtypePath. { intros h. apply impred; intro i. apply impred; intro j. apply impred; intro l. apply propproperty. } exact e. Defined.
imports: UniMath.MoreFoundations.Tactics UniMath.Combinatorics.FiniteSets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.Univalence UniMath.CategoryTheory.opp_precat