YES Time: 0.001200 TRS: {f f x -> g f x} DP: DP: {} TRS: {f f x -> g f x} Qed