proposition: Theorem dec_EqDec : forall (A : Set)(eqd : eq_dec A), EqDec A.
proof: Proof. intuition. eapply (Build_EqDec (fun a1 a2 => if (eqd a1 a2) then true else false)). intuition. destruct (eqd x y); trivial. discriminate. destruct (eqd x y); trivial. congruence. Qed.
imports: Bvector Arith