proposition: Lemma Forall_inv {A :Type}(P: A -> Prop)(n:nat) a v : Vector.Forall P (n:= S n) (Vector.cons a v) -> P a /\ Vector.Forall P v .
proof: Proof. intro H. inversion H. assert (v0 = v) by (refine (Eqdep_dec.inj_pair2_eq_dec nat _ _ _ _ _ H2); apply eq_nat_dec). now subst. Qed.