proposition: Lemma Aeq_Dec : forall x y:A, {x=y}+{x<>y}.
proof: Proof. intros. induction (sumbool_of_bool (Aeq x y)). apply left. assert (h:= (Aeq_spec x y)); rewrite a in h; assumption. apply right. assert (h:= (Aeq_spec x y)); rewrite b in h; assumption. Qed.
imports: Coq(List)