proposition: Lemma status_eq : forall f g, f =F= g -> tau f = tau g.
proof: Proof. intros f g f_eq_g. unfold tau, mytau; trivial. Qed.
imports: CoLoR(VPrecedence MultisetListOrder VRPO_Type VTerm ListUtil AccUtil LogicUtil) Coq(Relations) CoLoR(VRPO_Type)