The error message says:
Non-constant TAKE, WITNESS, or HAVE for temporal goal
so this restriction was an explicit design decision. (Not sure if it is documented anywhere ...)
Even with the explicit SUFFICES construct, your proof is likely to be doomed: at some point you'll have to apply temporal logic reasoning (the PTL method), and as a rule of thumb, in all temporal steps the context should only contain "boxed" assumptions, i.e., all assumptions A should be equivalent to []A. This is true for constant formulas A, formulas []A, <>[]A, WF_v(A) etc., but not for Spec, which will contain an initial state predicate.
If you continue your proof attempt, you'll find that PTL warns about "non-[] assumption" and fails. Invariant proofs should be written in the form
THEOREM Spec => []Invariant
<1>1. Init => Invariant
<1>2. Invariant /\ [][Next]_v => Invariant'
<1>. QED BY <1>1, <1>2, PTL DEF Spec
In particular, the context of the QED step is empty, so all its assumptions are "boxed".
Stephan