Definition uncurrify {n: nat} {v: vec UU n} {B: UU} (f: iterfun v B): hvec v → B. Proof. revert n v f. refine (vec_ind _ _ _). - intros. exact f. - intros x n xs IHxs f. simpl in *. intro a. exact (IHxs (f (pr1 a)) (pr2 a)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.Combinatorics.StandardFiniteSets.