fact: Definition ddp_step_min_wf R := rest (fun t => acc_sub R t /\ well_formed t) (ddp_step R).
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec) CoLoR(NatCompat)