proposition: Lemma to_list_length : forall (A : Set)(m : nat)(v : Vector.t A m), length (Vector.to_list v) = m.
proof: Proof. induction m; intuition. rewrite (vector_0 v). simpl. trivial. destruct (vector_S v). destruct H. subst. simpl. f_equal. eapply IHm. Qed.
imports: FCF.StdNat List Bvector micromega.Lia FCF.EqDec FCF.Fold ZArith