proposition: Lemma arpo_dec : rel_dec arpo.
proof: Proof. intros p q. destruct (VRPO_Results.rpo_lt_dec (vterm_of_aterm q) (vterm_of_aterm p)); intuition. Defined.
imports: CoLoR(ATrs VPrecedence VRPO_Status VRPO_Results VTerm_of_ATerm ListUtil Preorder SN RelUtil ARelation VSignature LogicUtil) Coq(Arith Wellfounded)