reduction of RecNat now only proceeds when certain arguments have
already been expanded