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. rewrite (eq_st f g f_eq_g). trivial. Qed.
imports: CoLoR(VPrecedence MultisetListOrder ListLex VRPO_Type VTerm ListUtil AccUtil LogicUtil) Coq(Relations)