proposition: Lemma leF_dec : rel_dec leF.
proof: Proof. intros x y. unfold ltF, ltA, leF, eqA. destruct (le_lt_dec (prec x) (prec y)); intuition. Defined.
imports: CoLoR(ATrs VPrecedence VRPO_Status VRPO_Results VTerm_of_ATerm ListUtil Preorder SN RelUtil ARelation VSignature LogicUtil) Coq(Arith Wellfounded)