proposition: Lemma to_list_Exists A P n (v : t A n): Exists P v <-> List.Exists 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; now constructor; auto. Qed.
imports: VectorDef PeanoNat Eqdep_dec