fact: Parameter th_eq_closure_one_step : forall (R : term -> term -> Prop), forall t1 t2, one_step (rwr R) t1 t2 -> rwr R t1 t2.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec)