proposition: Lemma flatten_apply_cf_subst : forall sigma f l, arity f = AC -> permut (flatten f (map (apply_cf_subst sigma) l)) (flatten f (apply_cf_subst sigma (build f l) :: nil)).
proof: Proof. intros sigma f l Af; induction l as [ | t1 l]. simpl; generalize (F.Symb.eq_bool_ok f f); case (F.Symb.eq_bool f f); [intros _ | intro f_diff_f; apply False_rect; apply f_diff_f; reflexivity]. rewrite Af; repeat rewrite quicksort_equation; simpl; auto. destruct l as [ | t2 l]; auto. simpl; rewrite Af; generalize (F.Symb.eq_bool_ok f f); case (F.Symb.eq_bool f f); [intros _ | intro f_diff_f; apply False_rect; apply f_diff_f; reflexivity]. rewrite <- app_nil_end; apply permut_sym; apply quick_permut_bis; transitivity (flatten f (map (apply_cf_subst sigma) (t1 :: t2 :: l))); auto; apply list_permut_flatten. apply permut_map with (@eq term). intros; subst; reflexivity. apply permut_sym; apply quick_permut. Qed.
imports: Coq(Relations List Arith Morphisms) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory_spec equational_theory)