proposition: Lemma unit_for_AC : forall f, arity f = AC -> match unit_theory f with | LU _ | RU _ => False | U _ | Nothing => True end.
proof: Proof. intros f Ar; generalize (unit_theory_is_coherent f); destruct (unit_theory f); trivial; intros [ H _ ]; rewrite Ar in H; discriminate. Qed.
imports: Coq(Arith List Relations) CoLoR(closure more_list weaved_relation list_sort term_spec equational_theory ac cf_eq_ac rpo)