Level based no dne get attr record

theorem level_based_no_dne_get_attr_record {e : Expr} {tx₁ : TypedExpr} {ty : CedarType} {rty : RecordType} {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)  (hl : (tx₁.getAttr a ty).AtLevel env n)  (ht : typeOf e c₀ env = Except.ok (tx₁, c₁))  (hrty : tx₁.typeOf = CedarType.record rty)  (ihe : TypedAtLevelHasNoDNEError e) :  evaluate (.getAttr e a) request entities ≠ .error .entityDoesNotExist:= by  cases hl  case getAttr hety =>    simp [hety] at hrty  rename_i hl₁  simp only [evaluate]  have ⟨ hgc, v, he, hi ⟩ := type_of_is_sound hc hr ht  unfold EvaluatesTo at he  rcases he with he | he | he | he  · exact absurd he (ihe hc hr hcl ht hl₁)  · simp [he]  · simp [he]  · rw [hrty] at hi    obtain ⟨ attrs, hv ⟩ := instance_of_record_type_is_record hi    subst hv    simp only [he, Except.bind_ok, getAttr, attrsOf, Map.findOrErr]    split <;> simp