proposition: 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: Proof. apply idpath. Defined.
imports: UniMath.Combinatorics.StandardFiniteSets UniMath.Foundations.NaturalNumbers