fact: Parameter size_size_aux3 : forall f t, arity f = AC -> well_formed t -> 1 <= length (A:=term) (flatten f (canonical_form t :: nil)).
imports: Coq(Relations List Arith Morphisms) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory_spec equational_theory)