Proving Progress for STLC with Linear and Unrestricted Types In this paper Walker presents an extension of STLC with linear and unrestricted types. The proof of type soundness is left as an exercise to the reader. I encountered difficulty when attempting to prove progress (in a theorem prover):

$$ \vdash (S_1,e_1) ~\Rightarrow~ \textsf{value}{(e_1)} ~\lor~ \exists S_2 \exists e_2.~ (S_1,e_1) \rightarrow (S_2,e_2)$$

The relevant typing and evaluation relations can be found on pages 6-17 of the linked document. If we attempt to prove progress by induction on the typing derivation, we encounter the following problem: there is a typing rule for variables, but variables are not values and the evaluation relation says nothing about variables.

Now adding a variable rule to the evaluation relation is the wrong solution. For example, we don't want to reduce $(\varnothing,\mathsf{un~true})$ to $(x\mapsto\mathsf{un~true},x)$, and the immediately reduce $x$ to $\mathsf{un~true}$ by looking up its value in the store. The two solutions I am considering are (1) adding variables to the set of values; and (2) requiring that terms reduce to variables or can take a step in the statement of the progress lemma. Ideally the correction would reflect the original intention of the author. It is also possible that I am misunderstanding the paper or language.
Variables can be considered as values if the evaluation strategy is call-by-value. Otherwise said, it only makes sense to substitute a variable with a value (in call-by-value). I am unable to check if that is the case in the paper you refer to since I can't access it.