proposition: Lemma length_flatten_ter : forall f sigma, arity f = AC -> well_formed_cf_subst sigma -> forall l, (forall t, In t l -> well_formed_cf t) -> length l <= length (flatten f (map (apply_cf_subst sigma) l)).
proof: Proof. intros f sigma Af Wsigma l Wl; induction l as [ | t l]; trivial. replace (t::l) with ((t::nil) ++ l); trivial; rewrite map_app; rewrite flatten_app; do 2 rewrite length_app; apply Nat.add_le_mono. assert (Wtsigma : well_formed_cf (apply_cf_subst sigma t)). apply well_formed_cf_apply_subst; trivial; apply Wl; left; trivial. simpl map; destruct (apply_cf_subst sigma t) as [ v | g ll ]; simpl; trivial; simpl; generalize (F.Symb.eq_bool_ok f g); case (F.Symb.eq_bool f g); [intros f_eq_g; subst g | intros _]; trivial. rewrite <- app_nil_end; apply Nat.le_trans with 2; auto with arith; apply well_formed_cf_length with f; trivial. apply IHl; intros; apply Wl; right; trivial. Qed.
imports: Coq(Relations List Arith Morphisms) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory_spec equational_theory)