proposition: Lemma beq_ko : forall x y, beq x y = false <-> x <> y.
proof: Proof. intros. destruct (beq_ok x y). case_eq (beq x y); intuition. rewrite H1 in H4. discr. Defined.
imports: Coq(Structures.Equalities) CoLoR(LogicUtil RelUtil BoolUtil)