Definition hvec_ind (P : ∏ n (v: vec UU n), hvec v → UU) : P 0 [()] [()] → (∏ X x n (v: vec UU n) (hv : hvec v), P n v hv → P (S n) (vcons X v) (x ::: hv)) → (∏ n (v: vec UU n) (hv : hvec v), P n v hv). Proof. intros H0 HI n v hv. induction n as [|n IHn]. - induction v, hv. exact H0. - change v with (pr1 v ::: pr2 v)%vec. change hv with (pr1 hv ::: pr2 hv). apply HI, IHn. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.Combinatorics.StandardFiniteSets.