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