Definition hvec_ind_fixedv {v:∏ n:nat, vec UU n} (P : ∏ n , hvec (v n) → UU) : (∏ hv0 , P 0 hv0) → (∏ n , (∏ hv , P n hv) → (∏ hv, P (S n) hv) ) → (∏ n (hv : hvec (v n)), P n hv). Proof. intros H0 HI n hv. induction n as [|n IHn]. - use H0. - change hv with (pr1 hv ::: pr2 hv). apply HI, IHn. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.Combinatorics.StandardFiniteSets.