proposition: Lemma to_list_Forall2 A B P n (v1 : t A n) (v2 : t B n) : Forall2 P v1 v2 <-> List.Forall2 P (to_list v1) (to_list v2).
proof: Proof. split; intros HF. - induction HF; now constructor. - remember (to_list v1) as l1. remember (to_list v2) as l2. revert n v1 v2 Heql1 Heql2; induction HF; intros n v1 v2 Heql1 Heql2. + destruct v1; [ | inversion Heql1 ]. apply case0; constructor. + destruct v1; inversion Heql1; subst. rewrite (eta v2) in Heql2; inversion Heql2; subst. rewrite (eta v2); constructor; auto. Qed.
imports: VectorDef PeanoNat Eqdep_dec