proposition: Lemma acc_one_step : forall R t, Acc (one_step R) t <-> Acc (rwr R) t.
proof: Proof. intros R t; split. apply acc_trans. apply Acc_incl; intros; left; assumption. Qed.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)