Definition iterfun {n: nat} (v: vec UU n) (B: UU): UU. Proof. revert n v. refine (vec_ind _ _ _). - exact B. - intros x n xs IHxs. exact (x → IHxs). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.Combinatorics.StandardFiniteSets.