proposition: Lemma mutate_c : forall f, arity f = C -> (unit_theory f = Nothing) -> forall s1 t1 s2 t2, well_formed s1 -> well_formed t1 -> well_formed s2 -> well_formed t2 -> acu (Term f (s1 :: t1 :: nil)) (Term f (s2 :: t2 :: nil)) -> (acu s1 s2 /\ acu t1 t2) \/ (acu s1 t2 /\ acu t1 s2).
proof: Proof. intros f Af UT s1 t1 s2 t2 Ws1 Wt1 Ws2 Wt2 H; generalize (acu_is_ac_on_unit_nf (Term f (s1 :: t1 :: nil)) (Term f (s2 :: t2 :: nil))); 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. assert (H' := Sort.quick_permut (canonical_form (unit_nf s1) :: canonical_form (unit_nf t1) :: nil)). rewrite H in H'; clear H. assert (H'' := Sort.quick_permut (canonical_form (unit_nf s2) :: canonical_form (unit_nf t2) :: nil)). assert (H := permut_trans H' (permut_sym H'')). clear H' H''. destruct (list_permut.permut_length_2 H) as [[s1_eq_s2 t1_eq_t2] | [s1_eq_t2 s2_eq_t1]]. left; split. generalize (acu_is_ac_on_unit_nf s1 s2); intros [H' _]; apply H'; apply cf_eq_ac; trivial. apply well_formed_unit_nf; trivial. apply well_formed_unit_nf; trivial. generalize (acu_is_ac_on_unit_nf t1 t2); intros [H' _]; apply H'; apply cf_eq_ac; trivial. apply well_formed_unit_nf; trivial. apply well_formed_unit_nf; trivial. right; split. generalize (acu_is_ac_on_unit_nf s1 t2); intros [H' _]; apply H'; apply cf_eq_ac; trivial. apply well_formed_unit_nf; trivial. apply well_formed_unit_nf; trivial. generalize (acu_is_ac_on_unit_nf t1 s2); intros [H' _]; apply H'; apply cf_eq_ac. apply well_formed_unit_nf; trivial. apply well_formed_unit_nf; trivial. unfold EDS.eq_A in *; trivial. Qed.
imports: Coq(Arith List Relations) CoLoR(closure more_list weaved_relation list_sort term_spec equational_theory ac cf_eq_ac rpo)