(VAR X) (RULES c -> f(g(c)) f(g(X)) -> g(X) )
Submit to AProVE Web Frontend
Edit in AProVE Web Frontend