Definition monfunstncomp { n m k : nat } ( f : monfunstn n m ) ( g : monfunstn m k ) : monfunstn n k . Proof. intros . exists ( g ∘ f ) . intros i j l. unfold funcomp. apply ( pr2 g ). apply ( pr2 f ) . assumption. Defined.
Require Import UniMath.MoreFoundations.Tactics.