proposition: Lemma dec_beq : forall x y : A, {x=y}+{~x=y}.
proof: Proof. intros. set (b := beq x y). case_eq b; intros. left. exact (proj1 (beq_ok x y) H). right. intro. unfold b in H. subst. rewrite beq_refl in H. discr. Defined.
imports: Coq(Structures.Equalities) CoLoR(LogicUtil RelUtil BoolUtil)