proposition: Lemma add_a_subterm_subst : forall f l1 l2' l2'' t sigma, arity f = AC -> well_formed_cf (Term f (l2' ++ t :: l2'')) -> apply_cf_subst sigma (build f l1) = build f (l2' ++ l2'') -> permut (flatten f (t :: (map (apply_cf_subst sigma) l1))) (l2' ++ t :: l2'').
proof: Proof. intros f l1 l2' l2'' t sigma Af Wt2 t1_sigma. assert (Al_t : match t with | Var _ => True | Term g ll => f <> g end). apply (well_formed_cf_alien Af Wt2); apply in_or_app; right; left; trivial. simpl; destruct t as [ v | g ll]. rewrite <- permut_cons_inside. refine (permut_trans (flatten_apply_cf_subst sigma l1 Af) _); rewrite t1_sigma; apply flatten_build_inside with (Var v); trivial. 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. intros _; rewrite <- permut_cons_inside. refine (permut_trans (flatten_apply_cf_subst sigma l1 Af) _); rewrite t1_sigma; apply flatten_build_inside with (Term g ll); trivial. reflexivity. Qed.
imports: Coq(Arith List) CoLoR(more_list list_sort term_spec ac cf_eq_ac matching matching_well_founded matching_well_formed)