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