Level based no dne get attr

theorem level_based_no_dne_get_attr {e : Expr} {a : Attr} {n : Nat} {c₀ c₁ : Capabilities} {env : TypeEnv} {request : Request} {entities : Entities}  (hc : CapabilitiesInvariant c₀ request entities)  (hr : InstanceOfWellFormedEnvironment request entities env)  (hcl : EntitiesClosedAtLevel entities request n)  (ht : typeOf (e.getAttr a) c₀ env = Except.ok (tx, c₁))  (hl : tx.AtLevel env n)  (ihe : TypedAtLevelHasNoDNEError e) :  evaluate (.getAttr e a) request entities ≠ .error .entityDoesNotExist:= by  have ⟨ _, tx₁, c₁', ht', h₅, h₆ ⟩ := type_of_getAttr_inversion ht  rw [h₅] at hl  cases h₆  case inl hety =>    obtain ⟨ ety, hety ⟩ := hety    exact level_based_no_dne_get_attr_entity hc hr hcl hl ht' hety ihe  case inr hrty =>    obtain ⟨ rty, hrty ⟩ := hrty    exact level_based_no_dne_get_attr_record hc hr hcl hl ht' hrty ihe