INIT Init
NEXT Next
INVARIANT TypeOk Impossible