Characterizing closure under expansion/reduction for big-step semantics?
The notion of "next" and "last" - prior to the idea of "expansion" and "reduction" - are  essentially lost when we read a big-step operational semantics as an inductive definition, which is too bad because the way we usually prove things about big-step operational semantics is by reading it as an inductive definition! 

You can prove a "full expansion" property (big step preservation) that $e \Downarrow v$ and $e \in R$ imply $v \in R$, and then observe that the proof of this property actually proves a small-step expansion property. This is because computational structure of the proof actually recovers the small-step evaluation process that Prolog/Twelf would use to execute the big-step semantics as a logic program! But for appropriately tricky semantics (especially non-deterministic ones), I've noticed it's frequently the case that you can prove a big-step property when it doesn't hold for the small-step evaluation process that Prolog/Twelf proof proof search would imply.

In my view, the best option - if we want to use big-step specifications but recover the information that was lost when we treated the big-step semantics as inductive definition - to characterize the small-step evaluation process that Prolog/Twelf would use. (This ends up basically or exactly being an abstract machine semantics.) This may not be satisfying depending on what it is you're trying to do, of course. There are a couple of versions of this: see Hannan and Miller or Ager, for instance. (There's also a bit about this in my thesis, some work I did with Ian Zerny, but I'll link to that when there's a thing to link to.) You could also carefully characterize a set of partial derivations of $e_1 \Downarrow v_1, \ldots, e_n \Downarrow v_n \vdash e \Downarrow v$ that corresponded to partial executions, but when I've contemplated this the details have seemed fraught enough that the abstract machine interpretation seems like a safer bet.