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