Would the following function:
invariant Body opIndex (Key k)
{ if (k in _cache)
{ ....
return _cache[k].bdy;
}
return null;
}
return values that were invariant, or would that type have to
be declared at the declaration of the type "Body"?