proposition: Lemma mutate_free_sound : forall f l1 l2, rwr_list acu l1 l2 -> acu (Term f l1) (Term f l2).
proof: Proof. intros f l1 l2 H; apply general_context. apply trans_clos_is_clos. apply trans_incl with (one_step_list acu); trivial. clear; intro l1; induction l1 as [ | a1 l1]; intros l2 H; inversion H; clear H; subst. apply rwr_list_cons; assumption. apply rwr_list_tail; apply IHl1; assumption. Qed.
imports: Coq(Arith List Relations) CoLoR(closure more_list weaved_relation list_sort term_spec equational_theory ac cf_eq_ac rpo)