proposition: Lemma to_list_Forall A P n (v : t A n): Forall P v <-> List.Forall P (to_list v).
proof: Proof. split; intros HF. - induction HF; now constructor. - remember (to_list v) as l. revert n v Heql; induction HF; intros n v Heql; destruct v; inversion Heql; subst; constructor; auto. Qed.
imports: VectorDef PeanoNat Eqdep_dec