Levels

[aaronjeline]

Issue #, if available:
N/A
Description of changes:
This PR adds levels to the cedar type system, and proves them sound.
In specific:

• Modifies the entity type to take a level
• Modifies typeOf to now take the level we are validating at
• Adds a new, stronger form of entity store well-formedness
• Proves a stronger type soundness theorem, that eliminates the possibility of entity-does-not-exist errors

What still needs to be done:

• There is one remaining lemma to be proved, but putting this up now for general feedback on structure
• Write/verify the slicing algo

An interesting note on the design of the levels RFC:
The theorem the levels RFC (and this PR) prove doesn't capture everything we want, as the in operator does not fail with an error when the entity is missing.