now remove_equal_tail removes arguments occurring in the substitution, like in ?f[x] x =?= S x   (allowing FO approximation)