proposition: Lemma Forall2_nth_order A: forall P n (v1 v2 : t A n), Forall2 P v1 v2 <-> forall i (Hi1 : i < n) (Hi2 : i < n), P (nth_order v1 Hi1) (nth_order v2 Hi2).
proof: Proof. intros P n v1 v2. rewrite Forall2_nth. split. - intros H i Hi1 Hi2. rewrite (nth_order_ext _ _ _ _ Hi1 Hi2). apply H. - intros H p. rewrite <- (Fin.of_nat_to_nat_inv p). apply H. Qed.
imports: VectorDef PeanoNat Eqdep_dec