proposition: Lemma no_need_of_instance' : forall (R : relation term) t1 t2, R t1 t2 -> axiom R t1 t2.
proof: Proof. intros R t1 t2 H. replace t1 with (apply_subst nil t1); [idtac | apply empty_subst_is_id]. replace t2 with (apply_subst nil t2); [idtac | apply empty_subst_is_id]. apply instance; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)