proposition: Lemma beq_trans : forall x y z, beq x y = true -> beq y z = true -> beq x z = true.
proof: Proof. intros. rewrite beq_ok in H. rewrite beq_ok in H0. assert (x = z). apply eq_trans with y; hyp. rewrite beq_ok. exact H1. Qed.
imports: Coq(Structures.Equalities) CoLoR(LogicUtil RelUtil BoolUtil)