proposition: Lemma size_size_aux3 : forall f t, arity f = AC -> well_formed t -> 1 <= length (A:=term) (flatten f (canonical_form t :: nil)).
proof: Proof. intros f t Ar Wt; apply (length_flatten (t :: nil) Ar); intros u In_u; elim In_u; clear In_u; intro In_u. subst u; trivial. contradiction. Qed.
imports: Coq(Relations List Arith Morphisms) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory_spec equational_theory)