proposition: Lemma to_list_In A a n (v : t A n): In a v <-> List.In a (to_list v).
proof: Proof. split. - intros HIn; induction HIn; now constructor. - induction v; intros HIn; inversion HIn; subst; constructor; auto. Qed.
imports: VectorDef PeanoNat Eqdep_dec