proposition: Lemma beq_dec_ko : forall x y, beq_dec x y = false <-> x <> y.
proof: Proof. intros. case (eq_dec x y); case_eq (beq_dec x y); intuition. subst y. rewrite beq_dec_refl in H. discr. rewrite beq_dec_ok in H. contr. Qed.
imports: Coq(Structures.Equalities) CoLoR(LogicUtil RelUtil BoolUtil)