proposition: Lemma length_flatten_bis : forall f, arity f = AC -> forall l, (forall t, In t l -> well_formed_cf t) -> (length l) <= length (flatten f l).
proof: Proof. intros f Af l Wl; induction l as [ | t l]. simpl; auto with arith. simpl; destruct t as [v | g ll]. simpl; apply le_n_S; apply IHl; intros; apply Wl; right; trivial. generalize (F.Symb.eq_bool_ok f g); case (F.Symb.eq_bool f g); [intro f_eq_g | intro f_diff_g]. rewrite length_app; replace (S (length l)) with (1 + length l); trivial; apply Nat.add_le_mono. assert (Wt : well_formed_cf (Term g ll)). apply Wl; left; trivial. unfold well_formed_cf in Wt; subst g; rewrite Af in Wt; destruct Wt as [_ [Lll _]]; auto with arith. apply IHl; intros; apply Wl; right; trivial. simpl; apply le_n_S; 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)