GitLab

Currently, it is hard to instantiate globalsG in adequacy if an initialized type of one global variable refers to another (one needs to unfold the definition of initialized) and impossible if there is a cycle.

This is a problem because building a cycle can happen by accident and the user would not know if they do not instantiate adequacy.

The right solution would be to use some ghost state to agree on the initialized types (leibniz equality should be enough).