proposition: Lemma mutate_free_lu : forall f g u l1 s2 t2, f <> g -> unit_theory f = Nothing -> unit_theory g = LU u -> acu (Term f l1) (Term g (s2 :: t2 :: nil)) -> acu (Term f l1) t2 /\ acu (Term u nil) s2.
proof: Proof. intros f g u l1 s2 t2 f_diff_g UTf UTg H; generalize (acu_is_ac_on_unit_nf (Term f l1) (Term g (s2 :: t2 :: nil))); intros [ _ H' ]; generalize (H' H); clear H' H; intro H; simpl in H; rewrite UTg in H. revert H; generalize (T.eq_bool_ok (unit_nf s2) (Term u nil)); case (T.eq_bool (unit_nf s2) (Term u nil)); [intro s2_eq_u | intro s2_diff_u]. intro H; split. generalize (acu_is_ac_on_unit_nf (Term f l1) t2); intros [H' _]; generalize (H' H); trivial. rewrite <- s2_eq_u. unfold acu, th_eq; apply rwr_incl with (sym_refl unit_one_step_at_top). clear t2 H; intros t1 t2 [H | [H | H]]; [left | right; left | right; right; trivial]; unfold union; right; trivial. apply th_sym; apply unit_nf_is_sound. intro H; absurd (f=g); trivial. rewrite UTf in H; generalize (ac_top_eq H); destruct l1 as [ | s1 [ | t1 [ | u1 l1]]]; trivial. Qed.
imports: Coq(Arith List Relations) CoLoR(closure more_list weaved_relation list_sort term_spec equational_theory ac cf_eq_ac rpo)