proposition: Theorem eqb_symm : forall (A : Set){eqd : EqDec A}(x y : A), eqb x y = eqb y x.
proof: Proof. intuition. case_eq (eqb x y); intuition. rewrite eqb_leibniz in H. subst. rewrite eqb_refl. trivial. case_eq (eqb y x); intuition. rewrite eqb_leibniz in H0; subst. rewrite eqb_refl in H. discriminate. Qed.
imports: Bvector Arith