proposition: Lemma status_lifting : forall f, lifting (tau f lt).
proof: Proof. intro f; unfold tau, mytau, lt, lifting. apply (lex_lifting lt_lpo). Qed.
imports: CoLoR(VPrecedence ListLex VRPO_Type VTerm ListUtil AccUtil LogicUtil) Coq(Relations) CoLoR(VRPO_Type)