proposition: Lemma arpo_wf : WF arpo.
proof: Proof. intro x. unfold arpo. set (t := vterm_of_aterm x). apply SN_Rof with t; trivial. apply Acc_transp_SN. apply Acc_incl with VRPO.lt. intuition. apply VRPO_Results.wf_lt. Qed.
imports: CoLoR(ATrs VPrecedence VRPO_Status VRPO_Results VTerm_of_ATerm ListUtil Preorder SN RelUtil ARelation VSignature LogicUtil) Coq(Arith Wellfounded)