Typecheck policy at level with environments no dne

theorem typecheck_policy_at_level_with_environments_no_dne {p : Policy} {schema : Schema} {n : Nat} {request : Request} {entities : Entities}  (he : ∃ env ∈ schema.environments, InstanceOfWellFormedEnvironment request entities env)  (hcl : EntitiesClosedAtLevel entities request n)  (htl : typecheckPolicyWithEnvironments (typecheckPolicyWithLevel · n) p schema = .ok ()) :  evaluate p.toExpr request entities ≠ .error .entityDoesNotExist:= by  replace htl : ∀ x ∈ schema.environments, ∃ tx, typecheckPolicyWithLevel p n x = .ok tx := by    simp only [typecheckPolicyWithEnvironments, Except.mapError] at htl    simp_do_let (checkEntities schema p.toExpr) as hes at htl    simp_do_let (List.mapM (typecheckPolicyWithLevel p n) schema.environments) as htl₁ at htl    replace htl₁ := List.forall₂_implies_all_left ∘ List.mapM_ok_iff_forall₂.mp $ htl₁    intro env he    specialize htl₁ env he    simp only [htl₁.imp, and_imp, imp_self, implies_true]  have ⟨env, ⟨he₁, hr⟩⟩ := he  specialize htl env he₁  replace ⟨_, htl⟩ := htl  exact typecheck_policy_with_level_no_dne hr hcl htl