proposition: Lemma ltF_wf : well_founded ltF.
proof: Proof. unfold ltF, ltA, eqA, leF. apply WF_transp_wf. unfold transp. apply WF_incl with (fun x y => prec x > prec y). intros p q pq. destruct pq. destruct (lt_eq_lt_dec (prec p) (prec q)) as [[pq | pq] | pq]; intuition. intro x. apply (@SN_Rof Sig nat prec gt) with (prec x); trivial. apply Acc_transp_SN. apply Acc_incl with lt. intuition. apply lt_wf. Qed.
imports: CoLoR(ATrs VPrecedence VRPO_Status VRPO_Results VTerm_of_ATerm ListUtil Preorder SN RelUtil ARelation VSignature LogicUtil) Coq(Arith Wellfounded)