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