proposition: Lemma eqF_sym : forall f g, f =F= g -> g =F= f.
proof: Proof. intros. destruct (eqA_equivalence Sig leF). apply leF_preorder. unfold eqF; intuition. Defined.
imports: CoLoR(VRPO_Type VTerm Preorder ListUtil RelUtil LogicUtil AccUtil) Coq(Peano_dec)