proposition: Lemma add_a_subterm : forall f l l' t, arity f = AC -> (well_formed_cf (Term f (l ++ t :: l'))) -> permut (flatten f (build f (l ++ l') :: t :: nil)) (l ++ t :: l').
proof: Proof. intros f l l' t Af W. assert (Al_t : match t with | Var _ => True | Term g ll => f <> g end). apply (well_formed_cf_alien Af W); apply in_or_app; right; left; trivial. replace (build f (l ++ l') :: t :: nil) with ((build f (l ++ l') :: nil) ++ (t :: nil)); trivial. rewrite flatten_app; replace (flatten f (t :: nil)) with (t :: nil). rewrite <- permut_add_inside. rewrite <- app_nil_end; apply flatten_build_inside with t; trivial. reflexivity. simpl; destruct t as [ v | g ll]. reflexivity. generalize (F.Symb.eq_bool_ok f g); case (F.Symb.eq_bool f g); [intro f_eq_g; apply False_rect; apply Al_t; assumption | reflexivity]. Qed.
imports: Coq(Arith List) CoLoR(more_list list_sort term_spec ac cf_eq_ac matching matching_well_founded matching_well_formed)