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