proposition: Lemma to_list_eq_inv : forall (A : Set) n (v1 v2 : Vector.t A n), VectorDef.to_list v1 = VectorDef.to_list v2 -> v1 = v2.
proof: Proof. induction n; intuition. rewrite (vector_0 v2). rewrite (vector_0 v1). trivial. destruct (vector_S v1). destruct (vector_S v2). destruct H0. destruct H1. subst. unfold VectorDef.to_list in *. inversion H; clear H; subst. f_equal. eauto. Qed.
imports: FCF.StdNat List Bvector micromega.Lia FCF.EqDec FCF.Fold ZArith Permutation