Level based no dne expr

theorem level_based_no_dne_expr {e : Expr} {n : Nat} {tx : TypedExpr} {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 c env = Except.ok (tx, c₁))  (hl : tx.AtLevel env n) :  evaluate e request entities ≠ .error .entityDoesNotExist:= by  cases e  case lit => simp [evaluate]  case var v => cases v <;> simp [evaluate]  case ite x₁ x₂ x₃ =>    have ih₁ := @level_based_no_dne_expr x₁    have ih₂ := @level_based_no_dne_expr x₂    have ih₃ := @level_based_no_dne_expr x₃    exact level_based_no_dne_if hc hr hcl ht hl ih₁ ih₂ ih₃  case and e₁ e₂ =>    have ih₁ := @level_based_no_dne_expr e₁    have ih₂ := @level_based_no_dne_expr e₂    exact level_based_no_dne_and hc hr hcl ht hl ih₁ ih₂  case or e₁ e₂ =>    have ih₁ := @level_based_no_dne_expr e₁    have ih₂ := @level_based_no_dne_expr e₂    exact level_based_no_dne_or hc hr hcl ht hl ih₁ ih₂  case unaryApp op e =>    have ihe := @level_based_no_dne_expr e    exact level_based_no_dne_unary_app hc hr hcl ht hl ihe  case binaryApp op e₁ e₂ =>    have ih₁ := @level_based_no_dne_expr e₁    have ih₂ := @level_based_no_dne_expr e₂    exact level_based_no_dne_binary_app hc hr hcl ht hl ih₁ ih₂  case getAttr e _ =>    have ihe := @level_based_no_dne_expr e    exact level_based_no_dne_get_attr hc hr hcl ht hl ihe  case hasAttr e _ =>    have ihe := @level_based_no_dne_expr e    exact level_based_no_dne_has_attr hc hr hcl ht hl ihe  case set xs =>    have ih : ∀ x ∈ xs, TypedAtLevelHasNoDNEError x := by      intro x hx      have _ : sizeOf x < sizeOf (Expr.set xs) := by        have h₁ := List.sizeOf_lt_of_mem hx        simp only [Expr.set.sizeOf_spec]        omega      exact @level_based_no_dne_expr x    exact level_based_no_dne_set hc hr hcl ht hl ih  case call xfn xs =>    have ih : ∀ x ∈ xs, TypedAtLevelHasNoDNEError x := by      intro x hx      have _ : sizeOf x < sizeOf (Expr.set xs) := by        have h₁ := List.sizeOf_lt_of_mem hx        simp only [Expr.set.sizeOf_spec]        omega      exact @level_based_no_dne_expr x    exact level_based_no_dne_call hc hr hcl ht hl ih  case record rxs =>    have ih : ∀ x ∈ rxs, TypedAtLevelHasNoDNEError x.snd := by      intro x hx      have _ : sizeOf x.snd < sizeOf (Expr.record rxs) := by        have h₁ := List.sizeOf_lt_of_mem hx        rw [Prod.mk.sizeOf_spec] at h₁        simp only [Expr.record.sizeOf_spec]        omega      exact @level_based_no_dne_expr x.snd    exact level_based_no_dne_record hc hr hcl ht hl ih