proposition: Lemma th_refl : forall R t, th_eq R t t.
proof: Proof. unfold th_eq, sym_refl. intros R t; apply t_step; apply at_top; rewrite <- (empty_subst_is_id t); apply instance; right; right; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)