proposition: Lemma vector_tl_eq : forall (A : Set)(n : nat)(v1 v2 : Vector.t A (S n)), v1 = v2 -> Vector.tl v1 = Vector.tl v2.
proof: Proof. intuition. specialize (vector_S v1). specialize (vector_S v2). intuition. destruct H0. destruct H0. destruct H1. destruct H1. subst. simpl. trivial. Qed.
imports: FCF.StdNat List Bvector micromega.Lia FCF.EqDec FCF.Fold ZArith