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