Definition stnprod { n : nat } ( f : ⟦n⟧ -> nat ) : nat. Proof. revert f. induction n as [ | n IHn ]. - intro. apply 1. - intro f. apply ( ( IHn ( λ i : ⟦n⟧, f ( dni lastelement i ) ) ) * f lastelement ). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.