proposition: 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: Proof. intros Hnil Hcons. induction n as [|m H]; intros. - apply (transportb (P 0) (vec0_eq v [()]) Hnil). - apply Hcons, H. Defined.
imports: UniMath.Combinatorics.StandardFiniteSets UniMath.Foundations.NaturalNumbers