fact: Definition ForallV_vector_tl n (v : vector T (S n)) (f : ForallV v) : ForallV (vector_tl v) := match f in @ForallV n v return match n as n return vector T n -> Prop with | 0 => fun _ => True | S _ => fun v => ForallV (vector_tl v) end v with | ForallV_nil => I | ForallV_cons _ _ _ _ pf => pf end.
imports: ExtLib.Data.Fin