Checked eval entity reachable

theorem checked_eval_entity_reachable {e : Expr} {n nmax: Nat} {c c' : Capabilities} {tx : TypedExpr} {env : TypeEnv} {request : Request} {entities : Entities} {v : Value} {path : List Attr} {euid : EntityUID}  (hc : CapabilitiesInvariant c request entities)  (hr : InstanceOfWellFormedEnvironment request entities env)  (ht : typeOf e c env = .ok (tx, c'))  (hl : tx.EntityAccessAtLevel env n nmax path)  (he : evaluate e request entities = .ok v)  (ha : Value.EuidViaPath v path euid) :  ReachableIn entities request.sliceEUIDs euid (n + 1):= by  cases e  case lit =>    have hi : euid ∈ request.sliceEUIDs := by      have hact := checked_eval_entity_lit_is_action hr ht he hl ha      simp [hact, Request.sliceEUIDs, Set.mem_union, Set.mem_make]    exact ReachableIn.in_start hi   case var =>    exact var_entity_reachable he ha   case ite e₁ e₂ e₃ =>    have ih₂ := @checked_eval_entity_reachable e₂    have ih₃ := @checked_eval_entity_reachable e₃    exact checked_eval_entity_reachable_ite hc hr ht hl he ha ih₂ ih₃   case and =>    exfalso    exact and_not_euid_via_path he ha   case or e=>    exfalso    exact or_not_euid_via_path he ha   case unaryApp op e =>    exfalso    exact unary_not_euid_via_path he ha   case binaryApp op e₁ e₂ =>    have ih₁ := @checked_eval_entity_reachable e₁    exact checked_eval_entity_reachable_binary hc hr ht hl he ha ih₁   case getAttr e _ =>    have ih := @checked_eval_entity_reachable e    exact checked_eval_entity_reachable_get_attr hc hr ht hl he ha ih   case hasAttr e a =>    exfalso    exact has_attr_not_euid_via_path he ha   case set es =>    exfalso    exact set_not_euid_via_path he ha   case record rxs =>    have ih : ∀ a x, (Map.make rxs).find? a = some x → CheckedEvalEntityReachable x := by      intros a x hfx      have : sizeOf x < sizeOf (Expr.record rxs) := by        replace he := Map.mem_make_mem_list (Map.find?_mem_toList hfx)        have h₁ := List.sizeOf_lt_of_mem he        rw [Prod.mk.sizeOf_spec a x] at h₁        simp only [Expr.record.sizeOf_spec, gt_iff_lt]        omega      exact @checked_eval_entity_reachable x    exact checked_eval_entity_reachable_record hc hr ht hl he ha ih   case call xfn args =>    exfalso    exact call_not_euid_via_path he ha