proposition: Lemma acc_eq_f : forall f g ss, f =F= g -> Acc lt (Fun f ss) -> Acc lt (Fun g ss).
proof: Proof. intros f g ss f_eq Hacc. inversion Hacc. constructor. intros t Ht. apply H. eapply (lt_eq_f Ht); trivial. Qed.
imports: CoLoR(VRPO_Type VTerm Preorder ListUtil RelUtil LogicUtil AccUtil) Coq(Peano_dec)