The sliced variant of typecheck_policy_with_level_no_dne (issue #642): evaluating
a level-checked policy against the level-n slice of a closed store also never
produces entityDoesNotExist. Follows trivially by transporting the full-store
result across the semantic-equivalence soundness theorem.
The _no_dne analogue of typecheck_policy_at_level_with_environments_is_sound:
a policy that level-checks against every environment of the schema (and so, in
particular, the one the request inhabits), evaluated against a store closed at
that level, never produces entityDoesNotExist.
Validator-level statement of issue #642: if every policy in ps validates at
level n and entities is closed at level n for the request, then no policy
evaluates to an entityDoesNotExist error. This is exactly the family of
evaluations isAuthorized performs, so it is the closure guarantee isAuthorized
inherits (the authorizer surfaces evaluation results only through the
kind-agnostic errorPolicies / satisfiedPolicies, and never introduces a
entityDoesNotExist of its own). Mirrors validate_with_level_is_sound_wf.