proposition: Lemma Forall2_nth A: forall P n (v1 v2 : t A n), Forall2 P v1 v2 <-> forall p, P (nth v1 p) (nth v2 p).
proof: Proof. intros P n v1 v2. split. - intros H. induction H. + apply Fin.case0. + intros p. now apply (Fin.caseS' p). - apply (fun P H1 H2 => rect2 P H1 H2 v1 v2). + constructor. + intros ??? IH ?? H. constructor. * apply (H Fin.F1). * apply IH. intros p. apply (H (Fin.FS p)). Qed.
imports: VectorDef PeanoNat Eqdep_dec