YES TRS: {f(f(a())) -> f(g())} RUF: Strict: {} Weak: {} Qed