Lemma vec_ind (P : ∏ n, vec A n → UU) : P 0 [()] → (∏ x n (v : vec A n), P n v → P (S n) (x ::: v)) → (∏ n (v : vec A n), P n v). Proof. intros Hnil Hcons. induction n as [|m H]; intros. - apply (transportb (P 0) (vec0_eq v [()]) Hnil). - apply Hcons, H. Defined.
Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Foundations.NaturalNumbers.