Level based no dne get attr entity

theorem level_based_no_dne_get_attr_entity {e : Expr} {tx₁ : TypedExpr} {ty : CedarType} {ety : EntityType} {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₁))  (hety : tx₁.typeOf = CedarType.entity ety)  (ihe : TypedAtLevelHasNoDNEError e) :  evaluate (.getAttr e a) request entities ≠ .error .entityDoesNotExist:= by  have ⟨ hgc, v, he, hv ⟩ := type_of_is_sound hc hr ht  rw [hety] at hv  replace ⟨ euid, hety', hv ⟩ := instance_of_entity_type_is_entity hv  subst hety' hv  cases hl  case getAttrRecord hnety _ =>    specialize hnety euid.ty    contradiction  rename_i n hel₁ hl₁ _  simp only [evaluate]  have hl₁' := entity_access_at_level_then_at_level hl₁  unfold EvaluatesTo at he  rcases he with he | he | he | he  · exact absurd he (ihe hc hr hcl ht hl₁')  · simp [he]  · simp [he]  · have hcont := checked_eval_entity_exists hc hr ht hl₁ he (.euid euid) hcl    obtain ⟨ ed, hed ⟩ := Map.contains_iff_some_find?.mp hcont    simp only [he, Except.bind_ok, getAttr, attrsOf, Entities.attrs, Map.findOrErr, hed]    split <;> simp