fact: Parameter size_size : forall t, well_formed t -> size t = ac_size (canonical_form t).
imports: Coq(Relations List Arith Morphisms) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory_spec equational_theory)