proposition: Lemma well_formed_cf_build_inside : forall f t l1 l2, arity f = AC -> well_formed_cf (Term f (l1 ++ t :: l2)) -> well_formed_cf (build f (l1 ++ l2)).
proof: Proof. intros f t l1 l2 Af W; assert (H : forall u, In u (l1 ++ l2) -> In u (l1 ++ t :: l2)). intros u In_u; elim (in_app_or _ _ _ In_u); clear In_u; intro In_u; apply in_or_app; [ left | right; right ]; trivial. apply well_formed_cf_build; trivial. apply le_S_n; replace (S (length (l1 ++ l2))) with (length (l1 ++ t :: l2)). apply well_formed_cf_length with f; trivial. do 2 rewrite length_app; rewrite Nat.add_comm; simpl; rewrite Nat.add_comm; trivial. intros u In_u; apply (well_formed_cf_subterms W); apply H; trivial. intros u In_u; apply (well_formed_cf_alien Af W); apply H; trivial. Qed.
imports: Coq(Relations List Arith Morphisms) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory_spec equational_theory)