proposition: Lemma beq_com : forall x y, beq x y = beq y x.
proof: Proof. intros. case_eq (beq x y); intros; sym. rewrite beq_ok. sym. rewrite <- beq_ok. hyp. rewrite beq_ko. cut (x<>y). auto. rewrite <- beq_ko. hyp. Qed.
imports: Coq(Structures.Equalities) CoLoR(LogicUtil RelUtil BoolUtil)