proposition: Lemma flatten_build : forall f l, arity f = AC -> (forall t, In t l -> match t with | Var _ => True | Term g _ => f <> g end) -> permut (flatten f ((build f l) :: nil)) l.
proof: Proof. intros f [ | t1 [ | t2 l]] Af Al. simpl; generalize (F.Symb.eq_bool_ok f f); case (F.Symb.eq_bool f f); [intros _; apply Pnil | intro f_diff_f; apply False_rect; apply f_diff_f; reflexivity]. assert (Al_t1 := Al _ (or_introl _ (eq_refl _))). simpl; destruct t1 as [ | g]; [auto | idtac]. generalize (F.Symb.eq_bool_ok f g); case (F.Symb.eq_bool f g); [intros f_eq_g | intros _]. apply False_rect; apply Al_t1; assumption. reflexivity. 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 <- app_nil_end; apply quick_permut_bis; auto. Qed.
imports: Coq(Relations List Arith Morphisms) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory_spec equational_theory)