proposition: Lemma ac_size_ge_one : forall t, well_formed_cf t -> 1 <= ac_size t.
proof: Proof. intros t Wt; elim (well_formed_cf_is_well_formed_cf _ Wt); intros u [Wu Hu]; subst; rewrite <- size_size; trivial; apply size_ge_one. Qed.
imports: Coq(Relations List Arith Morphisms) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory_spec equational_theory)