Lemma monfunstnpr1_isInjective {m n} (f g : monfunstn m n) : monfunstnpr1 f = monfunstnpr1 g -> f = g. Proof. intros e. apply subtypePath. { intros h. apply impred; intro i. apply impred; intro j. apply impred; intro l. apply propproperty. } exact e. Defined.
Require Import UniMath.MoreFoundations.Tactics.