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