proposition: Lemma vector_cons_ne : forall (A : Set)(n : nat)(a1 a2 : Vector.t A n)(a : A), a1 <> a2 -> Vector.cons A a n a1 <> Vector.cons A a n a2.
proof: Proof. intuition. eapply H. eapply vector_cons_eq. eauto. Qed.
imports: FCF.StdNat List Bvector micromega.Lia FCF.EqDec FCF.Fold ZArith