generic specification
parameter
elemdata
target
sorts store;
constants ∅ : store;
functions . [ . ] : store × elem × data → store;
variables st : store;
st0 : store;
st1 : store;
st2 : store;
induction store generated by ∅, [ ];
end generic specification