Lemma vec_ind_compute (P : ∏ n, vec A n → UU) {n:nat} {v:vec A n} {x:A} (H0 : P 0 [()]) (HI : ∏ x n (v : vec A n), P n v → P (S n) (x ::: v)) : (vec_ind P H0 HI) (S n) (x:::v) = HI x n v (vec_ind P H0 HI n v). Proof. apply idpath. Defined.
Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Foundations.NaturalNumbers.