fact: Parameter nf_one_step_subterm: forall R t, nf (one_step R) t -> forall s, direct_subterm s t -> nf (one_step R) s.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec)