proposition: Lemma status_lifting : forall f, lifting (tau f lt).
proof: Proof. intro f; unfold tau, mytau, lt. intro l; destruct (status f). apply (lex_lifting lt_rpo). apply (mult_lifting lt_rpo). unfold eqA, Term.eqA; intros; subst; trivial. unfold eqA, Term.eqA; intros; subst; trivial. Qed.
imports: CoLoR(VPrecedence MultisetListOrder ListLex VRPO_Type VTerm ListUtil AccUtil LogicUtil) Coq(Relations)