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