state and step predicate and variable types?

[ns]

Suppose I wanted to define a generic way of making a spec from components

mk(si) == si.init /\ [][si.next]_si.vars

so i could say something like

Init1 == x=0
Next1 == x'>x

vars1 == <<x>>
si == [init |-> Init1, next |-> Next1, vars |-> vars1]
Spec == mk(si)

If I wanted to declare the Record Type call it SpecInfo, what should the "types" of the various fields of SpecInfo be?

SpecInfo == [init:?, next:?, vars:?]

I can sort of see how I might be able to make the init and next fields be functions, but i'm not sure what to do with the vars field.

Thanks