proposition: Lemma unit_th_is_unit_nf_eq : forall t1 t2, unit_th t1 t2 <-> unit_nf t1 = unit_nf t2.
proof: Proof. intros t1 t2; split. intro H; induction H; [ idtac | apply trans_eq with (unit_nf y); trivial]; apply one_step_unit_th_unit_nf_eq; assumption. unfold unit_th, th_eq; intro H'; apply trans_clos_is_trans with (unit_nf t1); [idtac | rewrite H'; 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)