Definition hvec_ind' {n:nat} {v: vec UU n} (P : ∏ n' (v': vec UU n'), hvec v' → UU) : P 0 [()] [()] → (∏ X x m (w: vec UU m) (hw : hvec w), m<n → P m w hw → P (S m) (vcons X w) (x ::: hw)) → ∏ hv : hvec v, P n v hv. Proof. intros H0 HI 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. * apply natlthnsn. * apply IHn. intros X x m w hw Hm HIm. apply HI. + apply (istransnatlth _ n). ++ exact Hm. ++ apply natlthnsn. + exact HIm. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.Combinatorics.StandardFiniteSets.