First_Order_Rewriting.Rewrite_Relations_Impl