Within a precondition or postcondition expression for entry family E, denotes the value of the entry index for the call of E.
E’Index return entry_index_subtype
