Typecheck policy with level no dne

theorem typecheck_policy_with_level_no_dne {p : Policy} {tx : TypedExpr} {n : Nat} {env : TypeEnv} {request : Request} {entities : Entities}  (hr : InstanceOfWellFormedEnvironment request entities env)  (hcl : EntitiesClosedAtLevel entities request n)  (htl : typecheckPolicyWithLevel p n env = .ok tx) :  evaluate p.toExpr request entities ≠ .error .entityDoesNotExist:= by  simp only [typecheckPolicyWithLevel, typecheckPolicy] at htl  split at htl <;> try contradiction  rename_i tx' _ htx'  cases htl₁ : tx'.typeOf ⊑ .bool .anyBool <;> simp only [htl₁, Bool.false_eq_true, ↓reduceIte, Except.bind_err, Except.bind_ok, reduceCtorEq] at htl  split at htl <;> simp only [reduceCtorEq, Except.ok.injEq] at htl  subst htl  rename_i htl'  have subst_pres := (@substitute_action_preserves_evaluation · · entities)  rw [←subst_pres, action_matches_env hr]  rw [←level_spec] at htl'  exact level_based_no_dne_expr (empty_capabilities_invariant request entities) hr hcl htx' htl'