proposition: Lemma Forall2_inv {A B:Type}(P: A -> B -> Prop)(n:nat) a b v w : Vector.Forall2 P (n:=S n) (Vector.cons a v) (Vector.cons b w) -> P a b /\ Vector.Forall2 P v w.
proof: Proof. intro H. inversion H. assert (v1 = v) by (refine (Eqdep_dec.inj_pair2_eq_dec nat _ _ _ _ _ H2); apply eq_nat_dec). assert (v2 = w) by (refine (Eqdep_dec.inj_pair2_eq_dec nat _ _ _ _ _ H5); apply eq_nat_dec). subst; auto. Qed.