proposition: Lemma unit_nf_is_idempotent : forall t, unit_nf (unit_nf t) = unit_nf t.
proof: Proof. intro t; generalize (unit_th_is_unit_nf_eq (unit_nf t) t); intros [H _]; apply H; unfold unit_th; apply th_sym; apply unit_nf_is_sound. Qed.
imports: Coq(Arith List Relations) CoLoR(closure more_list weaved_relation list_sort term_spec equational_theory ac cf_eq_ac rpo)