proposition: Lemma ltF_dec : forall f g, {f <F g} + {~f <F g}.
proof: Proof. intros. unfold ltF, ltA, eqA. destruct (leF_dec f g). destruct (leF_dec g f). right. tauto. left. tauto. right. tauto. Defined.
imports: CoLoR(VRPO_Type VTerm Preorder ListUtil RelUtil LogicUtil AccUtil) Coq(Peano_dec)