YES Time: 0.000318 TRS: {f X -> g()} DP: DP: {} TRS: {f X -> g()} Qed