proposition: Lemma lt_status : forall f g, f =F= g -> forall ss ts, (forall t, In t ts -> lt t (Fun f ss)) -> tau f lt ts ss -> lt (Fun g ts) (Fun f ss).
proof: Proof. unfold lt, tau, mytau. intros f g feqg ss ts Hsub; apply mpo2; trivial. Qed.
imports: CoLoR(VPrecedence MultisetListOrder VRPO_Type VTerm ListUtil AccUtil LogicUtil) Coq(Relations) CoLoR(VRPO_Type)