fact: Parameter context_in : forall R t1 t2, rwr R t1 t2 -> forall f l l', rwr R (Term f (l ++ t1 :: l')) (Term f (l ++ t2 :: l')).
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec)