proposition: Lemma term_eq_bool_equiv : forall f g : M.term, f = g <-> M.eq_bool f g = true.
proof: Proof. intros f g. generalize (M.eq_bool_ok f g). case (eq_bool f g). tauto. intuition discriminate. Qed.
imports: Coq(List Bool) CoLoR(TransClosure)