proposition: Lemma beq_dec_trans : forall x y z, implb (beq_dec x y && beq_dec y z) (beq_dec x z) = true.
proof: Proof. intros. unfold beq_dec. case (eq_dec x y); case (eq_dec y z); case (eq_dec x z); intros; (refl || (cong || idtac)). Qed.
imports: Coq(Structures.Equalities) CoLoR(LogicUtil RelUtil BoolUtil)