proposition: Lemma eqbList_correct1 : forall (A : Set)(eqd : EqDec A) ls1 ls2, eqbList eqd ls1 ls2 = true -> ls1 = ls2.
proof: Proof. induction ls1; destruct ls2; intuition; simpl in *; try discriminate. apply andb_true_iff in H. intuition. f_equal. eapply eqb_leibniz. trivial. eauto. Qed.
imports: Bvector Arith