Definition foldright {E} (m : binop E) (e : E) {n : nat} (x: ⟦n⟧ -> E) : E. Proof. intros. induction n as [|n foldright]. + exact e. + exact (m (x firstelement) (foldright (x ∘ dni firstelement))). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.