proposition: Theorem EqDec_dec : forall A, EqDec A -> forall (a b : A), {a = b} + {a <> b}.
proof: Proof. intuition. remember (eqb a b) as x. destruct x. left. eapply eqb_leibniz. auto. right. intuition. subst. assert (eqb b b = true -> False). intuition. congruence. eapply H0. eapply eqb_leibniz. trivial. Qed.
imports: Bvector Arith