proposition: Lemma mutate_free : forall n f, arity f = Free n -> (unit_theory f = Nothing) -> forall l1 l2, (forall t, In t l1 -> well_formed t) -> (forall t, In t l2 -> well_formed t) -> acu (Term f l1) (Term f l2) -> l1 = l2 \/ rwr_list acu l1 l2.
proof: Proof. intros n f Af UT l1 l2 Wl1 Wl2 H; generalize (acu_is_ac_on_unit_nf (Term f l1) (Term f l2)); intros [ _ H']; generalize (ac_cf_eq (H' H)); clear H H'; intro H. do 2 rewrite unit_nf_nothing in H; trivial. simpl in H; rewrite Af in H; injection H; clear H; intro H; do 2 rewrite map_map in H; generalize l2 Wl2 H; clear f Af UT l2 Wl2 H; induction l1 as [ | s1 l1]; intros l2 Wl2 H; destruct l2 as [ | s2 l2]; trivial; try discriminate. left; trivial. simpl in H; injection H; clear H; intros H H'. assert (Ws1 := Wl1 _ (or_introl _ (eq_refl _))). assert (Ws2 := Wl2 _ (or_introl _ (eq_refl _))). right; generalize (acu_is_ac_on_unit_nf s1 s2); intros [ H'' _]; generalize (H'' (cf_eq_ac (well_formed_unit_nf _ Ws1) (well_formed_unit_nf _ Ws2) H')); destruct (IHl1 (tail_prop _ Wl1) l2 (tail_prop _ Wl2) H) as [l1_eq_l2 | l1_acu_l2]; simpl. subst; intro s1_eq_s2; apply rwr_list_cons; left; assumption. intro s1_eq_s2; apply rwr_list_split; trivial. left; assumption. Qed.
imports: Coq(Arith List Relations) CoLoR(closure more_list weaved_relation list_sort term_spec equational_theory ac cf_eq_ac rpo)