proposition: Lemma wf_inner_wf : well_founded (one_step R).
proof: Proof. intro t; apply acc_inner_acc. Qed.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure more_list weaved_relation term equational_theory_spec rwr_strategies dp rpo)