diff --git a/cedar-lean/Cedar/Spec/Entities.lean b/cedar-lean/Cedar/Spec/Entities.lean
index 026bf28b6..b61ddedfc 100644
--- a/cedar-lean/Cedar/Spec/Entities.lean
+++ b/cedar-lean/Cedar/Spec/Entities.lean
@@ -62,6 +62,9 @@ def Entities.tagsOrEmpty (es : Entities) (uid : EntityUID) : Map Tag Value :=
   | some d => d.tags
   | none   => Map.empty
 
+def Entities.remove (es : Entities) (uid : EntityUID) : Entities :=
+  es.filter (λ uid' _ => uid == uid')
+
 ----- Derivations -----
 
 deriving instance Repr, DecidableEq, Inhabited for EntityData
diff --git a/cedar-lean/Cedar/Thm/Validation/Levels.lean b/cedar-lean/Cedar/Thm/Validation/Levels.lean
index 46aa33fa9..2dce9bd73 100644
--- a/cedar-lean/Cedar/Thm/Validation/Levels.lean
+++ b/cedar-lean/Cedar/Thm/Validation/Levels.lean
@@ -37,12 +37,13 @@ open Cedar.Data
 open Cedar.Spec
 open Cedar.Validation
 
-theorem level_based_slicing_is_sound_expr {e : Expr} {n : Nat} {tx : TypedExpr} {c c₁ : Capabilities} {env : Environment} {request : Request} {entities slice : Entities}
-  (hs : slice = entities.sliceAtLevel request n)
+theorem level_based_slicing_is_sound_expr {e : Expr} {n nmax : Nat} {tx : TypedExpr} {c c₁ : Capabilities} {env : Environment} {request : Request} {entities slice : Entities}
+  (hn : nmax ≥ n)
+  (hs : slice = entities.sliceAtLevel request nmax)
   (hc : CapabilitiesInvariant c request entities)
   (hr : RequestAndEntitiesMatchEnvironment env request entities)
   (ht : typeOf e c env = Except.ok (tx, c₁))
-  (hl : TypedExpr.AtLevel tx n) :
+  (hl : TypedExpr.AtLevel tx n nmax) :
   evaluate e request entities = evaluate e request slice
 := by
   cases e
@@ -52,28 +53,28 @@ theorem level_based_slicing_is_sound_expr {e : Expr} {n : Nat} {tx : TypedExpr}
     have ihc := @level_based_slicing_is_sound_expr c
     have iht := @level_based_slicing_is_sound_expr t
     have ihe := @level_based_slicing_is_sound_expr e
-    exact level_based_slicing_is_sound_if hs hc hr ht hl ihc iht ihe
+    exact level_based_slicing_is_sound_if hn hs hc hr ht hl ihc iht ihe
   case and e₁ e₂ =>
     have ih₁ := @level_based_slicing_is_sound_expr e₁
     have ih₂ := @level_based_slicing_is_sound_expr e₂
-    exact level_based_slicing_is_sound_and hs hc hr ht hl ih₁ ih₂
+    exact level_based_slicing_is_sound_and hn hs hc hr ht hl ih₁ ih₂
   case or e₁ e₂ =>
     have ih₁ := @level_based_slicing_is_sound_expr e₁
     have ih₂ := @level_based_slicing_is_sound_expr e₂
-    exact level_based_slicing_is_sound_or hs hc hr ht hl ih₁ ih₂
+    exact level_based_slicing_is_sound_or hn hs hc hr ht hl ih₁ ih₂
   case unaryApp op e =>
     have ihe := @level_based_slicing_is_sound_expr e
-    exact level_based_slicing_is_sound_unary_app hs hc hr ht hl ihe
+    exact level_based_slicing_is_sound_unary_app hn hs hc hr ht hl ihe
   case binaryApp op e₁ e₂ =>
     have ihe₁ := @level_based_slicing_is_sound_expr e₁
     have ihe₂ := @level_based_slicing_is_sound_expr e₂
-    exact level_based_slicing_is_sound_binary_app hs hc hr ht hl ihe₁ ihe₂
+    exact level_based_slicing_is_sound_binary_app hn hs hc hr ht hl ihe₁ ihe₂
   case getAttr e _ =>
     have ihe := @level_based_slicing_is_sound_expr e
-    exact level_based_slicing_is_sound_get_attr hs hc hr ht hl ihe
+    exact level_based_slicing_is_sound_get_attr hn hs hc hr ht hl ihe
   case hasAttr e _ =>
     have ihe := @level_based_slicing_is_sound_expr e
-    exact level_based_slicing_is_sound_has_attr hs hc hr ht hl ihe
+    exact level_based_slicing_is_sound_has_attr hn hs hc hr ht hl ihe
   case set xs =>
     replace ⟨ hc, txs, ty,  htx, ht ⟩  := type_of_set_inversion ht
     subst tx
@@ -92,7 +93,7 @@ theorem level_based_slicing_is_sound_expr {e : Expr} {n : Nat} {tx : TypedExpr}
         simp only [Expr.record.sizeOf_spec]
         omega
       exact @level_based_slicing_is_sound_expr x.snd
-    exact level_based_slicing_is_sound_record hs hc hr ht hl ih
+    exact level_based_slicing_is_sound_record hn hs hc hr ht hl ih
 termination_by e
 
 theorem level_based_slicing_is_sound {p : Policy} {n : Nat} {env : Environment} {request : Request} {entities slice : Entities}
@@ -108,4 +109,4 @@ theorem level_based_slicing_is_sound {p : Policy} {n : Nat} {env : Environment}
   )
   rw [←level_spec] at htl
   have hc := empty_capabilities_invariant request entities
-  exact level_based_slicing_is_sound_expr hs hc hr ht htl
+  exact level_based_slicing_is_sound_expr (by omega) hs hc hr ht htl
diff --git a/cedar-lean/Cedar/Thm/Validation/Levels/And.lean b/cedar-lean/Cedar/Thm/Validation/Levels/And.lean
index 411c9884e..5b854f5c1 100644
--- a/cedar-lean/Cedar/Thm/Validation/Levels/And.lean
+++ b/cedar-lean/Cedar/Thm/Validation/Levels/And.lean
@@ -35,11 +35,12 @@ open Cedar.Spec
 open Cedar.Validation
 
 theorem level_based_slicing_is_sound_and {e₁ e₂ : Expr} {n : Nat} {c₀ c₁: Capabilities} {env : Environment} {request : Request} {entities slice : Entities}
-  (hs : slice = entities.sliceAtLevel request n)
+  (hn : nmax ≥ n)
+  (hs : slice = entities.sliceAtLevel request nmax)
   (hc : CapabilitiesInvariant c₀ request entities)
   (hr : RequestAndEntitiesMatchEnvironment env request entities)
   (ht : typeOf (.and e₁ e₂) c₀ env = Except.ok (tx, c₁))
-  (hl : TypedExpr.AtLevel tx n)
+  (hl : TypedExpr.AtLevel tx n nmax)
   (ih₁ : TypedAtLevelIsSound e₁)
   (ih₂ : TypedAtLevelIsSound e₂)
   : evaluate (.and e₁ e₂) request entities = evaluate (.and e₁ e₂) request slice
@@ -54,7 +55,7 @@ theorem level_based_slicing_is_sound_and {e₁ e₂ : Expr} {n : Nat} {c₀ c₁
     replace hv₁ := instance_of_ff_is_false hv₁
     subst v₁
     cases hl ; rename_i hl₁
-    specialize ih₁ hs hc hr htx₁ (by assumption)
+    specialize ih₁ hn hs hc hr htx₁ (by assumption)
     simp only [evaluate, ←ih₁]
     rcases he₁ with he₁ | he₁ | he₁ | he₁ <;>
     simp [he₁, Result.as, Coe.coe, Value.asBool]
@@ -63,11 +64,11 @@ theorem level_based_slicing_is_sound_and {e₁ e₂ : Expr} {n : Nat} {c₀ c₁
     replace ⟨ b₁ , hv₁⟩ := instance_of_bool_is_bool hv₁
     subst v₁ tx
     cases hl ; rename_i hl₁ hl₂
-    specialize ih₁ hs hc hr htx₁ hl₁
+    specialize ih₁ hn hs hc hr htx₁ hl₁
     simp only [evaluate, ←ih₁]
     rcases he₁ with he₁ | he₁ | he₁ | he₁ <;>
     simp only [he₁, Result.as, Bool.not_eq_eq_eq_not, Bool.not_true, Coe.coe, Value.asBool, Except.bind_err]
     cases b₁ <;> simp only [Except.bind_ok, ↓reduceIte]
     specialize hgc he₁
-    specialize ih₂ hs (capability_union_invariant hc hgc) hr htx₂ hl₂
+    specialize ih₂ hn hs (capability_union_invariant hc hgc) hr htx₂ hl₂
     simp [ih₂]
diff --git a/cedar-lean/Cedar/Thm/Validation/Levels/Basic.lean b/cedar-lean/Cedar/Thm/Validation/Levels/Basic.lean
index fa7408a5e..e51e039f9 100644
--- a/cedar-lean/Cedar/Thm/Validation/Levels/Basic.lean
+++ b/cedar-lean/Cedar/Thm/Validation/Levels/Basic.lean
@@ -26,10 +26,11 @@ Basic definitions for levels proof
 open Cedar.Spec
 open Cedar.Validation
 
-def TypedAtLevelIsSound (e : Expr) : Prop := ∀ {n : Nat} {tx : TypedExpr} {c c₁ : Capabilities} {env :Environment} {request : Request} {entities slice : Entities},
-  slice = entities.sliceAtLevel request n →
+def TypedAtLevelIsSound (e : Expr) : Prop := ∀ {n nmax : Nat} {tx : TypedExpr} {c c₁ : Capabilities} {env :Environment} {request : Request} {entities slice : Entities},
+  nmax >= n →
+  slice = entities.sliceAtLevel request nmax→
   CapabilitiesInvariant c request entities →
   RequestAndEntitiesMatchEnvironment env request entities →
   typeOf e c env = Except.ok (tx, c₁) →
-  TypedExpr.AtLevel tx n →
+  TypedExpr.AtLevel tx n nmax →
   evaluate e request entities = evaluate e request slice
diff --git a/cedar-lean/Cedar/Thm/Validation/Levels/BinaryApp.lean b/cedar-lean/Cedar/Thm/Validation/Levels/BinaryApp.lean
index 44100028a..1f14057f1 100644
--- a/cedar-lean/Cedar/Thm/Validation/Levels/BinaryApp.lean
+++ b/cedar-lean/Cedar/Thm/Validation/Levels/BinaryApp.lean
@@ -45,27 +45,32 @@ theorem not_dereferencing_apply₂_invariant_entities {op : BinaryOp} {entities
       cases p₁ <;> cases p₂ <;> simp
     )
 
-theorem level_based_slicing_is_sound_inₑ {e₁ : Expr} {euid₁ euid₂ : EntityUID} {n : Nat} {c₀ c₁ : Capabilities} {entities slice : Entities}
+theorem level_based_slicing_is_sound_inₑ {e₁ : Expr} {euid₁ euid₂ : EntityUID} {n nmax : Nat} {c₀ c₁ : Capabilities} {entities slice : Entities}
+  (hn : nmax ≥ n + 1)
   (hc : CapabilitiesInvariant c₀ request entities)
   (hr : RequestAndEntitiesMatchEnvironment env request entities)
   (ht : typeOf e₁ c₀ env = Except.ok (tx₁, c₁))
-  (hl : TypedExpr.AtLevel tx₁ n)
+  (hl : TypedExpr.AtLevel tx₁ n nmax)
   (hel : ¬ TypedExpr.EntityLitViaPath tx₁ [])
   (he : evaluate e₁ request entities = .ok (Value.prim (Prim.entityUID euid₁)))
-  (hs : some slice = entities.sliceAtLevel request (n + 1))
+  (hs : some slice = entities.sliceAtLevel request nmax)
   : inₑ euid₁ euid₂ entities = inₑ euid₁ euid₂ slice
 := by
   simp only [inₑ]
   cases heq : euid₁ == euid₂ <;> simp only [Bool.false_or, Bool.true_or]
+  replace hl : TypedExpr.AtLevel tx₁ (nmax - 1) nmax :=
+    check_level_greater (by omega) hl
+  rw [(by simp at hn ; omega : nmax = nmax - 1 + 1)] at hs
   have hfeq := checked_eval_entity_find_entities_eq_find_slice hc hr ht hl hel he hs
   simp [hfeq, Entities.ancestorsOrEmpty]
 
 theorem level_based_slicing_is_sound_binary_app {op : BinaryOp} {e₁ e₂ : Expr} {n : Nat} {c₀ c₁: Capabilities} {env : Environment} {request : Request} {entities slice : Entities}
-  (hs : slice = entities.sliceAtLevel request n)
+  (hn : nmax ≥ n)
+  (hs : slice = entities.sliceAtLevel request nmax)
   (hc : CapabilitiesInvariant c₀ request entities)
   (hr : RequestAndEntitiesMatchEnvironment env request entities)
   (ht : typeOf (.binaryApp op e₁ e₂) c₀ env = Except.ok (tx, c₁))
-  (hl : TypedExpr.AtLevel tx n)
+  (hl : TypedExpr.AtLevel tx n nmax)
   (ihe₁ : TypedAtLevelIsSound e₁)
   (ihe₂ : TypedAtLevelIsSound e₂)
   : evaluate (.binaryApp op e₁ e₂) request entities = evaluate (.binaryApp op e₁ e₂) request slice
@@ -75,10 +80,10 @@ theorem level_based_slicing_is_sound_binary_app {op : BinaryOp} {e₁ e₂ : Exp
   simp only [evaluate]
   cases hl
   case getTag hel hl₁ hl₂ | hasTag hel hl₁ hl₂ =>
-    specialize ihe₂ hs hc hr htx₂ hl₂
+    specialize ihe₂ (by omega) hs hc hr htx₂ hl₂
     rw [←ihe₂]
     have hl₁' := check_level_succ hl₁
-    specialize ihe₁ hs hc hr htx₁ hl₁'
+    specialize ihe₁ hn hs hc hr htx₁ hl₁'
     rw [←ihe₁]
     cases he₁ : evaluate e₁ request entities <;> simp only [Except.bind_ok, Except.bind_err]
     cases he₂ : evaluate e₂ request entities <;> simp only [Except.bind_ok, Except.bind_err]
@@ -87,13 +92,16 @@ theorem level_based_slicing_is_sound_binary_app {op : BinaryOp} {e₁ e₂ : Exp
     rename_i p₁ p₂
     cases p₁ <;> cases p₂ <;> simp only
     rename_i euid _
+    replace hl₁ : TypedExpr.AtLevel tx₁ (nmax - 1) nmax :=
+      check_level_greater (by omega) hl₁
+    rw [(by simp at hn ; omega : nmax = nmax - 1 + 1)] at hs
     have hfeq := checked_eval_entity_find_entities_eq_find_slice hc hr htx₁ hl₁ hel he₁ hs
     simp only [hfeq, hasTag, getTag, Entities.tagsOrEmpty, Entities.tags, Map.findOrErr]
   case mem hel hl₁ hl₂ =>
-    specialize ihe₂ hs hc hr htx₂ hl₂
+    specialize ihe₂ (by omega) hs hc hr htx₂ hl₂
     rw [←ihe₂]
     have hl₁' := check_level_succ hl₁
-    specialize ihe₁ hs hc hr htx₁ hl₁'
+    specialize ihe₁ hn hs hc hr htx₁ hl₁'
     rw [←ihe₁]
     cases he₁ : evaluate e₁ request entities <;> simp only [Except.bind_ok, Except.bind_err]
     cases he₂ : evaluate e₂ request entities <;> simp only [Except.bind_ok, Except.bind_err]
@@ -102,13 +110,13 @@ theorem level_based_slicing_is_sound_binary_app {op : BinaryOp} {e₁ e₂ : Exp
     case prim =>
       rename_i p₁ p₂
       cases p₁ <;> cases p₂ <;> simp only
-      simp [level_based_slicing_is_sound_inₑ hc hr htx₁ hl₁ hel he₁ hs]
+      simp [level_based_slicing_is_sound_inₑ hn hc hr htx₁ hl₁ hel he₁ hs]
     case set =>
       rename_i p₁ sv
       cases p₁ <;> simp only
-      simp [inₛ, level_based_slicing_is_sound_inₑ hc hr htx₁ hl₁ hel he₁ hs]
+      simp [inₛ, level_based_slicing_is_sound_inₑ hn hc hr htx₁ hl₁ hel he₁ hs]
   case binaryApp hop hl₁ hl₂ =>
-    specialize ihe₁ hs hc hr htx₁ hl₁
-    specialize ihe₂ hs hc hr htx₂ hl₂
+    specialize ihe₁ hn hs hc hr htx₁ hl₁
+    specialize ihe₂ hn hs hc hr htx₂ hl₂
     rw [ihe₁, ihe₂]
     simp [(@not_dereferencing_apply₂_invariant_entities op entities slice · · hop)]
diff --git a/cedar-lean/Cedar/Thm/Validation/Levels/CheckLevel.lean b/cedar-lean/Cedar/Thm/Validation/Levels/CheckLevel.lean
index 976b0e0f6..fc726f3d9 100644
--- a/cedar-lean/Cedar/Thm/Validation/Levels/CheckLevel.lean
+++ b/cedar-lean/Cedar/Thm/Validation/Levels/CheckLevel.lean
@@ -151,77 +151,77 @@ def DereferencingBinaryOp : BinaryOp → Prop
   | .mem | .hasTag | .getTag => True
   | _ => False
 
-inductive TypedExpr.AtLevel : TypedExpr → Nat → Prop where
-  | lit (p : Prim) (ty : CedarType) (n : Nat) :
-    AtLevel (.lit p ty) n
-  | var (v : Var) (ty : CedarType) (n : Nat) :
-    AtLevel (.var v ty) n
-  | ite (tx₁ tx₂ tx₃ : TypedExpr) (ty : CedarType) (n : Nat)
-    (hl₁ : AtLevel tx₁ n)
-    (hl₂ : AtLevel tx₂ n)
-    (hl₃ : AtLevel tx₃ n) :
-    AtLevel (.ite tx₁ tx₂ tx₃ ty) n
-  | and (tx₁ tx₂ : TypedExpr) (ty : CedarType) (n : Nat)
-    (hl₁ : AtLevel tx₁ n)
-    (hl₂ : AtLevel tx₂ n) :
-    AtLevel (.and tx₁ tx₂ ty) n
+inductive TypedExpr.AtLevel : TypedExpr → Nat → Nat → Prop where
+  | lit (p : Prim) (ty : CedarType) (n nmax : Nat) :
+    AtLevel (.lit p ty) n nmax
+  | var (v : Var) (ty : CedarType) (n nmax : Nat) :
+    AtLevel (.var v ty) n nmax
+  | ite (tx₁ tx₂ tx₃ : TypedExpr) (ty : CedarType) (n nmax : Nat)
+    (hl₁ : AtLevel tx₁ nmax nmax)
+    (hl₂ : AtLevel tx₂ n nmax)
+    (hl₃ : AtLevel tx₃ n nmax) :
+    AtLevel (.ite tx₁ tx₂ tx₃ ty) n nmax
+  | and (tx₁ tx₂ : TypedExpr) (ty : CedarType) (n nmax : Nat)
+    (hl₁ : AtLevel tx₁ n nmax)
+    (hl₂ : AtLevel tx₂ n nmax) :
+    AtLevel (.and tx₁ tx₂ ty) n nmax
   | or (tx₁ tx₂ : TypedExpr) (ty : CedarType) (n : Nat)
-    (hl₁ : AtLevel tx₁ n)
-    (hl₂ : AtLevel tx₂ n) :
-    AtLevel (.or tx₁ tx₂ ty) n
-  | unaryApp (op : UnaryOp) (tx₁ : TypedExpr) (ty : CedarType)
-    (hl₁ : AtLevel tx₁ n) :
-    AtLevel (.unaryApp op tx₁ ty) n
-  | mem (tx₁ tx₂ : TypedExpr) (ty : CedarType) (n : Nat)
+    (hl₁ : AtLevel tx₁ n nmax)
+    (hl₂ : AtLevel tx₂ n nmax) :
+    AtLevel (.or tx₁ tx₂ ty) n nmax
+  | unaryApp (op : UnaryOp) (tx₁ : TypedExpr) (ty : CedarType) (n nmax : Nat)
+    (hl₁ : AtLevel tx₁ n nmax) :
+    AtLevel (.unaryApp op tx₁ ty) n nmax
+  | mem (tx₁ tx₂ : TypedExpr) (ty : CedarType) (n nmax : Nat)
     (he : ¬ EntityLitViaPath tx₁ [])
-    (hl₁ : AtLevel tx₁ n)
-    (hl₂ : AtLevel tx₂ (n + 1)) :
-    AtLevel (.binaryApp .mem tx₁ tx₂ ty) (n + 1)
-  | getTag (tx₁ tx₂ : TypedExpr) (ty : CedarType) (n : Nat)
+    (hl₁ : AtLevel tx₁ n nmax)
+    (hl₂ : AtLevel tx₂ nmax nmax) :
+    AtLevel (.binaryApp .mem tx₁ tx₂ ty) (n + 1) nmax
+  | getTag (tx₁ tx₂ : TypedExpr) (ty : CedarType) (n nmax : Nat)
     (he : ¬ EntityLitViaPath tx₁ [])
-    (hl₁ : AtLevel tx₁ n)
-    (hl₂ : AtLevel tx₂ (n + 1)) :
-    AtLevel (.binaryApp .getTag tx₁ tx₂ ty) (n + 1)
-  | hasTag (tx₁ tx₂ : TypedExpr) (ty : CedarType) (n : Nat)
+    (hl₁ : AtLevel tx₁ n nmax)
+    (hl₂ : AtLevel tx₂ nmax nmax) :
+    AtLevel (.binaryApp .getTag tx₁ tx₂ ty) (n + 1) nmax
+  | hasTag (tx₁ tx₂ : TypedExpr) (ty : CedarType) (n nmax : Nat)
     (he : ¬ EntityLitViaPath tx₁ [])
-    (hl₁ : AtLevel tx₁ n)
-    (hl₂ : AtLevel tx₂ (n + 1)) :
-    AtLevel (.binaryApp .hasTag tx₁ tx₂ ty) (n + 1)
+    (hl₁ : AtLevel tx₁ n nmax)
+    (hl₂ : AtLevel tx₂ nmax nmax) :
+    AtLevel (.binaryApp .hasTag tx₁ tx₂ ty) (n + 1) nmax
   | binaryApp (op : BinaryOp) (tx₁ tx₂ : TypedExpr) (ty : CedarType) (n : Nat)
     (hop : ¬ DereferencingBinaryOp op)
-    (hl₁ : AtLevel tx₁ n)
-    (hl₂ : AtLevel tx₂ n) :
-    AtLevel (.binaryApp op tx₁ tx₂ ty) n
-  | getAttr (tx₁ : TypedExpr) (a : Attr) (ty : CedarType) {ety : EntityType} (n : Nat)
+    (hl₁ : AtLevel tx₁ n nmax)
+    (hl₂ : AtLevel tx₂ n nmax) :
+    AtLevel (.binaryApp op tx₁ tx₂ ty) n nmax
+  | getAttr (tx₁ : TypedExpr) (a : Attr) (ty : CedarType) {ety : EntityType} (n nmax : Nat)
     (he : ¬ EntityLitViaPath tx₁ [])
-    (hl₁ : AtLevel tx₁ n)
+    (hl₁ : AtLevel tx₁ n nmax)
     (hty : tx₁.typeOf = .entity ety) :
-    AtLevel (.getAttr tx₁ a ty) (n + 1)
-  | hasAttr (tx₁ : TypedExpr) (a : Attr) (ty : CedarType) {ety : EntityType} (n : Nat)
+    AtLevel (.getAttr tx₁ a ty) (n + 1) nmax
+  | hasAttr (tx₁ : TypedExpr) (a : Attr) (ty : CedarType) {ety : EntityType} (n nmax : Nat)
     (he : ¬ EntityLitViaPath tx₁ [])
-    (hl₁ : AtLevel tx₁ n)
+    (hl₁ : AtLevel tx₁ n nmax)
     (hty : tx₁.typeOf = .entity ety) :
-    AtLevel (.hasAttr tx₁ a ty) (n + 1)
-  | getAttrRecord (tx₁ : TypedExpr) (a : Attr) (ty : CedarType) (n : Nat)
-    (hl₁ : AtLevel tx₁ n)
+    AtLevel (.hasAttr tx₁ a ty) (n + 1) nmax
+  | getAttrRecord (tx₁ : TypedExpr) (a : Attr) (ty : CedarType) (n nmax : Nat)
+    (hl₁ : AtLevel tx₁ n nmax)
     (hty : ∀ ety, tx₁.typeOf ≠ .entity ety) :
-    AtLevel (.getAttr tx₁ a ty) n
-  | hasAttrRecord (tx₁ : TypedExpr) (a : Attr) (ty : CedarType) (n : Nat)
-    (hl₁ : AtLevel tx₁ n)
+    AtLevel (.getAttr tx₁ a ty) n nmax
+  | hasAttrRecord (tx₁ : TypedExpr) (a : Attr) (ty : CedarType) (n nmax : Nat)
+    (hl₁ : AtLevel tx₁ n nmax)
     (hty : ∀ ety, tx₁.typeOf ≠ .entity ety) :
-    AtLevel (.hasAttr tx₁ a ty) n
-  | set (txs : List TypedExpr) (ty : CedarType) (n : Nat)
-    (hl : ∀ tx ∈ txs, AtLevel tx n) :
-    AtLevel (.set txs ty) n
-  | record (attrs : List (Attr × TypedExpr)) (ty : CedarType)
-    (hl : ∀ atx ∈ attrs, AtLevel atx.snd n) :
-    AtLevel (.record attrs ty) n
-  | call (xfn : ExtFun) (args : List TypedExpr) (ty : CedarType)
-    (hl : ∀ tx ∈ args, AtLevel tx n) :
-    AtLevel (.call xfn args ty) n
+    AtLevel (.hasAttr tx₁ a ty) n nmax
+  | set (txs : List TypedExpr) (ty : CedarType) (n nmax : Nat)
+    (hl : ∀ tx ∈ txs, AtLevel tx n nmax) :
+    AtLevel (.set txs ty) n nmax
+  | record (attrs : List (Attr × TypedExpr)) (ty : CedarType) (n nmax : Nat)
+    (hl : ∀ atx ∈ attrs, AtLevel atx.snd n nmax) :
+    AtLevel (.record attrs ty) n nmax
+  | call (xfn : ExtFun) (args : List TypedExpr) (ty : CedarType) (n nmax : Nat)
+    (hl : ∀ tx ∈ args, AtLevel tx n nmax) :
+    AtLevel (.call xfn args ty) n nmax
 
-theorem level_spec {tx : TypedExpr} {n : Nat}:
-  (TypedExpr.AtLevel tx n ) ↔ (checkLevel tx n = true)
+theorem level_spec {tx : TypedExpr} {n nmax : Nat}:
+  (TypedExpr.AtLevel tx n nmax) ↔ (checkLevel tx n nmax = true)
 := by
   cases tx
   case lit =>
@@ -378,9 +378,10 @@ theorem level_spec {tx : TypedExpr} {n : Nat}:
       exact h₁
 termination_by tx
 
-theorem check_level_succ {tx : TypedExpr} {n : Nat}
-  (h₁ : TypedExpr.AtLevel tx n) :
-  TypedExpr.AtLevel tx (n + 1)
+
+theorem check_level_succ {tx : TypedExpr} {n nmax : Nat}
+  (h₁ : TypedExpr.AtLevel tx n nmax) :
+  TypedExpr.AtLevel tx (n + 1) nmax
 := by
   cases h₁
   case call htx | set htx =>
@@ -409,3 +410,9 @@ theorem check_level_succ {tx : TypedExpr} {n : Nat}
       try apply check_level_succ
       try assumption
     )
+
+theorem check_level_greater {tx : TypedExpr} {n n' nmax : Nat}
+  (hn : n ≤ n')
+  (h₁ : TypedExpr.AtLevel tx n nmax) :
+  TypedExpr.AtLevel tx n' nmax
+:= Nat.le.rec h₁ (λ _ ih => check_level_succ ih) hn
diff --git a/cedar-lean/Cedar/Thm/Validation/Levels/GetAttr.lean b/cedar-lean/Cedar/Thm/Validation/Levels/GetAttr.lean
index 1af83369c..58bff0d4c 100644
--- a/cedar-lean/Cedar/Thm/Validation/Levels/GetAttr.lean
+++ b/cedar-lean/Cedar/Thm/Validation/Levels/GetAttr.lean
@@ -35,11 +35,12 @@ open Cedar.Data
 open Cedar.Spec
 open Cedar.Validation
 
-theorem level_based_slicing_is_sound_get_attr_entity {e : Expr} {tx₁: TypedExpr} {ty : CedarType} {a : Attr} {n : Nat} {c₀ c₁: Capabilities} {env : Environment} {request : Request} {entities slice : Entities}
-  (hs : slice = entities.sliceAtLevel request n)
+theorem level_based_slicing_is_sound_get_attr_entity {e : Expr} {tx₁: TypedExpr} {ty : CedarType} {a : Attr} {n nmax: Nat} {c₀ c₁: Capabilities} {env : Environment} {request : Request} {entities slice : Entities}
+  (hn : nmax ≥ n)
+  (hs : slice = entities.sliceAtLevel request nmax)
   (hc : CapabilitiesInvariant c₀ request entities)
   (hr : RequestAndEntitiesMatchEnvironment env request entities)
-  (hl : TypedExpr.AtLevel (tx₁.getAttr a ty) n)
+  (hl : TypedExpr.AtLevel (tx₁.getAttr a ty) n nmax)
   (ht : typeOf e c₀ env = Except.ok (tx₁, c₁))
   (hety : tx₁.typeOf = CedarType.entity ety)
   (ihe : TypedAtLevelIsSound e)
@@ -53,20 +54,24 @@ theorem level_based_slicing_is_sound_get_attr_entity {e : Expr} {tx₁: TypedExp
   case getAttrRecord hnety _ =>
     specialize hnety euid.ty
     contradiction
-  rename_i n hel₁ hl₁ _
+  rename_i n hel₁ _ hl₁
   simp only [evaluate]
-  specialize ihe hs hc hr ht (check_level_succ hl₁)
+  specialize ihe (by omega) hs hc hr ht hl₁
   rw [←ihe]
   unfold EvaluatesTo at he
   rcases he with he | he | he | he <;> simp only [he, Except.bind_err]
+  replace hl₁ : TypedExpr.AtLevel tx₁ (nmax - 1) nmax :=
+    check_level_greater (by omega) hl₁
+  rw [(by omega : nmax = nmax - 1 + 1)] at hs
   have hfeq := checked_eval_entity_find_entities_eq_find_slice hc hr ht hl₁ hel₁ he hs
   simp [hfeq, getAttr, attrsOf, Entities.attrs, Map.findOrErr]
 
 theorem level_based_slicing_is_sound_get_attr_record {e : Expr} {tx : TypedExpr} {a : Attr} {n : Nat} {c₀: Capabilities} {env : Environment} {request : Request} {entities slice : Entities}
-  (hs : slice = entities.sliceAtLevel request n)
+  (hn : nmax ≥ n)
+  (hs : slice = entities.sliceAtLevel request nmax)
   (hc : CapabilitiesInvariant c₀ request entities)
   (hr : RequestAndEntitiesMatchEnvironment env request entities)
-  (hl : TypedExpr.AtLevel (ty₁.getAttr a tx.typeOf) n)
+  (hl : TypedExpr.AtLevel (ty₁.getAttr a tx.typeOf) n nmax)
   (ht : typeOf e c₀ env = Except.ok (ty₁, c₁'))
   (hrty : ty₁.typeOf = CedarType.record rty)
   (ihe : TypedAtLevelIsSound e)
@@ -77,10 +82,10 @@ theorem level_based_slicing_is_sound_get_attr_record {e : Expr} {tx : TypedExpr}
   replace ⟨ euid, h₁₄⟩ := instance_of_record_type_is_record h₁₄
   subst h₁₄
   cases hl
-  case getAttr hety =>
+  case getAttr hety _  =>
     simp [hety] at hrty
   rename_i hl
-  have ih := ihe hs hc hr ht hl
+  have ih := ihe hn  hs hc hr ht hl
   simp [evaluate, ←ih]
   cases he : evaluate e request entities <;> simp [he]
   simp [getAttr]
@@ -91,11 +96,12 @@ theorem level_based_slicing_is_sound_get_attr_record {e : Expr} {tx : TypedExpr}
   simp [attrsOf]
 
 theorem level_based_slicing_is_sound_get_attr {e : Expr} {tx : TypedExpr} {a : Attr} {n : Nat} {c₀ c₁: Capabilities} {env : Environment} {request : Request} {entities slice : Entities}
-  (hs : slice = entities.sliceAtLevel request n)
+  (hn : nmax ≥ n)
+  (hs : slice = entities.sliceAtLevel request nmax)
   (hc : CapabilitiesInvariant c₀ request entities)
   (hr : RequestAndEntitiesMatchEnvironment env request entities)
   (ht : typeOf (e.getAttr a) c₀ env = Except.ok (tx, c₁))
-  (hl : TypedExpr.AtLevel tx n)
+  (hl : TypedExpr.AtLevel tx n nmax)
   (ihe : TypedAtLevelIsSound e)
   : evaluate (.getAttr e a) request entities = evaluate (.getAttr e a) request slice
 := by
@@ -104,7 +110,7 @@ theorem level_based_slicing_is_sound_get_attr {e : Expr} {tx : TypedExpr} {a : A
   cases h₆
   case _ hety =>
     replace ⟨ ety, hety ⟩ := hety
-    exact level_based_slicing_is_sound_get_attr_entity hs hc hr hl ht hety ihe
+    exact level_based_slicing_is_sound_get_attr_entity hn hs hc hr hl ht hety ihe
   case _ hrty =>
     replace ⟨ rty, hrty ⟩ := hrty
-    exact level_based_slicing_is_sound_get_attr_record hs hc hr hl ht hrty ihe
+    exact level_based_slicing_is_sound_get_attr_record hn hs hc hr hl ht hrty ihe
diff --git a/cedar-lean/Cedar/Thm/Validation/Levels/HasAttr.lean b/cedar-lean/Cedar/Thm/Validation/Levels/HasAttr.lean
index 992d3a390..446bf757f 100644
--- a/cedar-lean/Cedar/Thm/Validation/Levels/HasAttr.lean
+++ b/cedar-lean/Cedar/Thm/Validation/Levels/HasAttr.lean
@@ -20,10 +20,11 @@ open Cedar.Spec
 open Cedar.Validation
 
 theorem level_based_slicing_is_sound_has_attr_entity {e : Expr} {tx₁: TypedExpr} {ty : CedarType} {a : Attr} {n : Nat} {c₀ c₁: Capabilities} {env : Environment} {request : Request} {entities slice : Entities}
-  (hs : slice = entities.sliceAtLevel request n)
+  (hn : nmax ≥ n)
+  (hs : slice = entities.sliceAtLevel request nmax)
   (hc : CapabilitiesInvariant c₀ request entities)
   (hr : RequestAndEntitiesMatchEnvironment env request entities)
-  (hl : TypedExpr.AtLevel (tx₁.hasAttr a ty) n)
+  (hl : TypedExpr.AtLevel (tx₁.hasAttr a ty) n nmax)
   (ht : typeOf e c₀ env = Except.ok (tx₁, c₁))
   (hety : tx₁.typeOf = CedarType.entity ety)
   (ihe : TypedAtLevelIsSound e)
@@ -37,20 +38,24 @@ theorem level_based_slicing_is_sound_has_attr_entity {e : Expr} {tx₁: TypedExp
   case hasAttrRecord hnety _ =>
     specialize hnety euid.ty
     contradiction
-  rename_i n hel₁ hl₁ _
+  rename_i n hel₁ _ hl₁
   simp [evaluate]
-  specialize ihe hs hc hr ht (check_level_succ hl₁)
+  specialize ihe hn hs hc hr ht (check_level_succ hl₁)
   rw [←ihe]
   unfold EvaluatesTo at he
   rcases he with he | he | he | he <;> simp [he]
+  replace hl₁ : TypedExpr.AtLevel tx₁ (nmax - 1) nmax :=
+    check_level_greater (by omega) hl₁
+  rw [(by simp at hn ; omega : nmax = nmax - 1 + 1)] at hs
   have hfeq := checked_eval_entity_find_entities_eq_find_slice hc hr ht hl₁ hel₁ he hs
   simp [hfeq, hasAttr, attrsOf, Entities.attrsOrEmpty]
 
 theorem level_based_slicing_is_sound_has_attr_record {e : Expr} {tx : TypedExpr} {a : Attr} {n : Nat} {c₀: Capabilities} {env : Environment} {request : Request} {entities slice : Entities}
-  (hs : slice = entities.sliceAtLevel request n)
+  (hn : nmax ≥ n)
+  (hs : slice = entities.sliceAtLevel request nmax)
   (hc : CapabilitiesInvariant c₀ request entities)
   (hr : RequestAndEntitiesMatchEnvironment env request entities)
-  (hl : TypedExpr.AtLevel (ty₁.hasAttr a tx.typeOf) n)
+  (hl : TypedExpr.AtLevel (ty₁.hasAttr a tx.typeOf) n nmax)
   (ht : typeOf e c₀ env = Except.ok (ty₁, c₁'))
   (hrty : ty₁.typeOf = CedarType.record rty)
   (ihe : TypedAtLevelIsSound e)
@@ -61,10 +66,10 @@ theorem level_based_slicing_is_sound_has_attr_record {e : Expr} {tx : TypedExpr}
   replace ⟨ euid, h₁₄⟩ := instance_of_record_type_is_record h₁₄
   subst h₁₄
   cases hl
-  case hasAttr hety =>
+  case hasAttr hety _ =>
     simp [hety] at hrty
   rename_i hl
-  have ih := ihe hs hc hr ht hl
+  have ih := ihe hn hs hc hr ht hl
   simp [evaluate, ←ih]
   cases he : evaluate e request entities <;> simp [he]
   simp [hasAttr]
@@ -75,11 +80,12 @@ theorem level_based_slicing_is_sound_has_attr_record {e : Expr} {tx : TypedExpr}
   simp [attrsOf]
 
 theorem level_based_slicing_is_sound_has_attr {e : Expr} {tx : TypedExpr} {a : Attr} {n : Nat} {c₀ c₁: Capabilities} {env : Environment} {request : Request} {entities slice : Entities}
-  (hs : slice = entities.sliceAtLevel request n)
+  (hn : nmax ≥ n)
+  (hs : slice = entities.sliceAtLevel request nmax)
   (hc : CapabilitiesInvariant c₀ request entities)
   (hr : RequestAndEntitiesMatchEnvironment env request entities)
   (ht : typeOf (e.hasAttr a) c₀ env = Except.ok (tx, c₁))
-  (hl : TypedExpr.AtLevel tx n)
+  (hl : TypedExpr.AtLevel tx n nmax)
   (ihe : TypedAtLevelIsSound e)
   : evaluate (.hasAttr e a) request entities = evaluate (.hasAttr e a) request slice
 := by
@@ -88,7 +94,7 @@ theorem level_based_slicing_is_sound_has_attr {e : Expr} {tx : TypedExpr} {a : A
   cases h₆
   case _ hety =>
     replace ⟨ ety, hety ⟩ := hety
-    exact level_based_slicing_is_sound_has_attr_entity hs hc hr hl ht hety ihe
+    exact level_based_slicing_is_sound_has_attr_entity hn hs hc hr hl ht hety ihe
   case _ hrty =>
     replace ⟨ rty, hrty ⟩ := hrty
-    exact level_based_slicing_is_sound_has_attr_record hs hc hr hl ht hrty ihe
+    exact level_based_slicing_is_sound_has_attr_record hn hs hc hr hl ht hrty ihe
diff --git a/cedar-lean/Cedar/Thm/Validation/Levels/IfThenElse.lean b/cedar-lean/Cedar/Thm/Validation/Levels/IfThenElse.lean
index bc87fc3d3..2d30cdf6c 100644
--- a/cedar-lean/Cedar/Thm/Validation/Levels/IfThenElse.lean
+++ b/cedar-lean/Cedar/Thm/Validation/Levels/IfThenElse.lean
@@ -34,11 +34,12 @@ open Cedar.Spec
 open Cedar.Validation
 
 theorem level_based_slicing_is_sound_if {c t e : Expr} {n : Nat} {c₀ c₁: Capabilities} {env : Environment} {request : Request} {entities slice : Entities}
-  (hs : slice = entities.sliceAtLevel request n)
+  (hn : nmax ≥ n)
+  (hs : slice = entities.sliceAtLevel request nmax)
   (hc : CapabilitiesInvariant c₀ request entities)
   (hr : RequestAndEntitiesMatchEnvironment env request entities)
   (ht : typeOf (.ite c t e) c₀ env = Except.ok (tx, c₁))
-  (hl : TypedExpr.AtLevel tx n)
+  (hl : TypedExpr.AtLevel tx n nmax)
   (ihc : TypedAtLevelIsSound c)
   (iht : TypedAtLevelIsSound t)
   (ihe : TypedAtLevelIsSound e)
@@ -50,10 +51,10 @@ theorem level_based_slicing_is_sound_if {c t e : Expr} {n : Nat} {c₀ c₁: Cap
     rw [htx] at hl
     cases hl
     rename_i hl₁ hl₂ hl₃
-    specialize ihc hs hc hr h₆ hl₁
+    specialize ihc (by omega) hs hc hr h₆ hl₁
     split at h₈
     · replace ⟨h₇, h₈, h₉⟩ := h₈
-      specialize ihe hs hc hr h₇ hl₃
+      specialize ihe hn hs hc hr h₇ hl₃
       subst h₉
       replace h₁₄ := instance_of_ff_is_false h₁₄
       subst h₁₄
@@ -83,10 +84,10 @@ theorem level_based_slicing_is_sound_if {c t e : Expr} {n : Nat} {c₀ c₁: Cap
       simp only [EvaluatesTo, ihc, h₁₅, reduceCtorEq, Except.ok.injEq, Value.prim.injEq, Prim.bool.injEq, false_or] at h₁₃
       subst h₁₃
       simp only [GuardedCapabilitiesInvariant, ihc, h₁₅, forall_const] at hgc
-      specialize iht hs (capability_union_invariant hc hgc) hr h₇ hl₂
+      specialize iht hn hs (capability_union_invariant hc hgc) hr h₇ hl₂
       simp [iht]
     · replace ⟨h₇, h₈, h₉, h₁₀⟩ := h₈
-      specialize ihe hs hc hr h₈ hl₃
+      specialize ihe hn hs hc hr h₈ hl₃
       simp only [ihc, ihe, evaluate]
       cases h₁₂ : Result.as Bool (evaluate c request slice) <;> simp only [Except.bind_err, Except.bind_ok]
       simp only [Result.as, Coe.coe, Value.asBool] at h₁₂
@@ -98,5 +99,5 @@ theorem level_based_slicing_is_sound_if {c t e : Expr} {n : Nat} {c₀ c₁: Cap
       case false => simp
       case true =>
         simp only [GuardedCapabilitiesInvariant, ihc, h₁₄, forall_const] at hgc
-        specialize iht hs (capability_union_invariant hc hgc) hr h₇ hl₂
+        specialize iht hn hs (capability_union_invariant hc hgc) hr h₇ hl₂
         simp [iht]
diff --git a/cedar-lean/Cedar/Thm/Validation/Levels/Or.lean b/cedar-lean/Cedar/Thm/Validation/Levels/Or.lean
index 66c95770f..c148b5b32 100644
--- a/cedar-lean/Cedar/Thm/Validation/Levels/Or.lean
+++ b/cedar-lean/Cedar/Thm/Validation/Levels/Or.lean
@@ -35,11 +35,12 @@ open Cedar.Spec
 open Cedar.Validation
 
 theorem level_based_slicing_is_sound_or {e₁ e₂ : Expr} {n : Nat} {c₀ c₁: Capabilities} {env : Environment} {request : Request} {entities slice : Entities}
-  (hs : slice = entities.sliceAtLevel request n)
+  (hn : nmax ≥ n)
+  (hs : slice = entities.sliceAtLevel request nmax)
   (hc : CapabilitiesInvariant c₀ request entities)
   (hr : RequestAndEntitiesMatchEnvironment env request entities)
   (ht : typeOf (.or e₁ e₂) c₀ env = Except.ok (tx, c₁))
-  (hl : TypedExpr.AtLevel tx n)
+  (hl : TypedExpr.AtLevel tx n nmax)
   (ih₁ : TypedAtLevelIsSound e₁)
   (ih₂ : TypedAtLevelIsSound e₂)
   : evaluate (.or e₁ e₂) request entities = evaluate (.or e₁ e₂) request slice
@@ -57,7 +58,7 @@ theorem level_based_slicing_is_sound_or {e₁ e₂ : Expr} {n : Nat} {c₀ c₁:
     simp [evaluate]
     cases hl
     rename_i hl₁ hl₂
-    specialize ih₁ hs hc hr htx₁ hl₁
+    specialize ih₁ hn hs hc hr htx₁ hl₁
     rw [←ih₁]
     rcases he₁ with he₁ | he₁ | he₁ | he₁ <;>
     simp [he₁, Result.as, Coe.coe, Value.asBool]
@@ -66,7 +67,7 @@ theorem level_based_slicing_is_sound_or {e₁ e₂ : Expr} {n : Nat} {c₀ c₁:
     subst tx
     cases hl
     rename_i hl₁ hl₂
-    specialize ih₁ hs hc hr htx₁ hl₁
-    specialize ih₂ hs hc hr htx₂ hl₂
+    specialize ih₁ hn hs hc hr htx₁ hl₁
+    specialize ih₂ hn hs hc hr htx₂ hl₂
     simp [evaluate]
     rw [ih₁, ih₂]
diff --git a/cedar-lean/Cedar/Thm/Validation/Levels/Record.lean b/cedar-lean/Cedar/Thm/Validation/Levels/Record.lean
index 097876529..ed2a55c95 100644
--- a/cedar-lean/Cedar/Thm/Validation/Levels/Record.lean
+++ b/cedar-lean/Cedar/Thm/Validation/Levels/Record.lean
@@ -34,11 +34,12 @@ open Cedar.Spec
 open Cedar.Validation
 
 theorem level_based_slicing_is_sound_record_attrs {rxs : List (Attr × Expr)} {n : Nat} {c : Capabilities} {env : Environment} {request : Request} {entities slice : Entities}
-  (hs : slice = entities.sliceAtLevel request n)
+  (hn : nmax ≥ n)
+  (hs : slice = entities.sliceAtLevel request nmax)
   (hc : CapabilitiesInvariant c request entities)
   (hr : RequestAndEntitiesMatchEnvironment env request entities)
   (ht : List.Forall₂ (AttrExprHasAttrType c env) rxs atxs)
-  (hl : ∀ atx ∈ atxs, TypedExpr.AtLevel atx.snd n)
+  (hl : ∀ atx ∈ atxs, TypedExpr.AtLevel atx.snd n nmax)
   (ih : ∀ x ∈ rxs, TypedAtLevelIsSound x.snd)
   :
   (rxs.mapM₂ λ x => do
@@ -56,21 +57,22 @@ theorem level_based_slicing_is_sound_record_attrs {rxs : List (Attr × Expr)} {n
     replace ⟨ ihx, ih ⟩ := ih
     replace ⟨ hlx, hl ⟩ := hl
     replace ⟨ _, _, htx ⟩ := htx
-    specialize ihx hs hc hr htx hlx
+    specialize ihx hn hs hc hr htx hlx
     simp only [←ihx, List.mapM₂, List.attach₂, List.pmap_cons, List.mapM_cons]
     cases he₁ : evaluate x.snd request entities <;> simp only [Except.bind_err, Except.bind_ok]
-    have ih' := level_based_slicing_is_sound_record_attrs hs hc hr ht hl ih
+    have ih' := level_based_slicing_is_sound_record_attrs hn hs hc hr ht hl ih
     simp only [List.mapM₂, List.attach₂] at ih'
     simp only [List.mapM_pmap_subtype (λ x : (Attr × Expr) => do let v ← evaluate x.snd request entities; .ok (x.fst, v)) rxs'] at ih' ⊢
     simp only [List.mapM_pmap_subtype (λ x : (Attr × Expr) => do let v ← evaluate x.snd request slice; .ok (x.fst, v)) rxs'] at ih' ⊢
     rw [ih']
 
 theorem level_based_slicing_is_sound_record {rxs : List (Attr × Expr)} {n : Nat} {c₀ c₁: Capabilities} {env : Environment} {request : Request} {entities slice : Entities}
-  (hs : slice = entities.sliceAtLevel request n)
+  (hn : nmax ≥ n)
+  (hs : slice = entities.sliceAtLevel request nmax)
   (hc : CapabilitiesInvariant c₀ request entities)
   (hr : RequestAndEntitiesMatchEnvironment env request entities)
   (ht : typeOf (.record rxs) c₀ env = Except.ok (tx, c₁))
-  (hl : TypedExpr.AtLevel tx n)
+  (hl : TypedExpr.AtLevel tx n nmax)
   (ih : ∀ x ∈ rxs, TypedAtLevelIsSound x.snd) :
   evaluate (.record rxs) request entities = evaluate (.record rxs) request slice
 := by
@@ -78,5 +80,5 @@ theorem level_based_slicing_is_sound_record {rxs : List (Attr × Expr)} {n : Nat
   subst htx
   cases hl
   rename_i hlatxs
-  have h := level_based_slicing_is_sound_record_attrs hs hc hr hatxs hlatxs ih
+  have h := level_based_slicing_is_sound_record_attrs hn hs hc hr hatxs hlatxs ih
   simp [h, evaluate, bindAttr]
diff --git a/cedar-lean/Cedar/Thm/Validation/Levels/Slice.lean b/cedar-lean/Cedar/Thm/Validation/Levels/Slice.lean
index 41f2a139b..9caeee744 100644
--- a/cedar-lean/Cedar/Thm/Validation/Levels/Slice.lean
+++ b/cedar-lean/Cedar/Thm/Validation/Levels/Slice.lean
@@ -106,11 +106,11 @@ theorem in_val_then_val_slice
   case set | ext => cases hv
 
 def CheckedEvalEntityReachable (e : Expr) :=
-  ∀ {n : Nat} {c c' : Capabilities} {tx : TypedExpr} {env : Environment} {request : Request} {entities : Entities} {v: Value} {path : List Attr} {euid : EntityUID},
+  ∀ {n nmax: Nat} {c c' : Capabilities} {tx : TypedExpr} {env : Environment} {request : Request} {entities : Entities} {v: Value} {path : List Attr} {euid : EntityUID},
     CapabilitiesInvariant c request entities →
     RequestAndEntitiesMatchEnvironment env request entities →
     typeOf e c env = .ok (tx, c') →
-    TypedExpr.AtLevel tx n →
+    TypedExpr.AtLevel tx n nmax →
     ¬ TypedExpr.EntityLitViaPath tx path →
     evaluate e request entities = .ok v →
     Value.EuidViaPath v path euid →
@@ -160,7 +160,7 @@ theorem checked_eval_entity_reachable_ite {e₁ e₂ e₃: Expr} {n : Nat} {c c'
   (hc : CapabilitiesInvariant c request entities)
   (hr : RequestAndEntitiesMatchEnvironment env request entities)
   (ht : typeOf (.ite e₁ e₂ e₃) c env = .ok (tx, c'))
-  (hl : TypedExpr.AtLevel tx n)
+  (hl : TypedExpr.AtLevel tx n nmax)
   (hel : ¬ TypedExpr.EntityLitViaPath tx path)
   (he : evaluate (.ite e₁ e₂ e₃) request entities = .ok v)
   (ha : Value.EuidViaPath v path euid)
@@ -292,7 +292,7 @@ theorem checked_eval_entity_reachable_binary {op : BinaryOp} {e₁ e₂: Expr} {
   (hc : CapabilitiesInvariant c request entities)
   (hr : RequestAndEntitiesMatchEnvironment env request entities)
   (ht : typeOf (.binaryApp op e₁ e₂) c env = .ok (tx, c'))
-  (hl : TypedExpr.AtLevel tx n)
+  (hl : TypedExpr.AtLevel tx n nmax)
   (hel : ¬ TypedExpr.EntityLitViaPath tx path)
   (he : evaluate (.binaryApp op e₁ e₂) request entities = .ok v)
   (ha : Value.EuidViaPath v path euid)
@@ -362,7 +362,7 @@ theorem checked_eval_entity_reachable_get_attr {e : Expr} {n : Nat} {c c' : Capa
   (hc : CapabilitiesInvariant c request entities)
   (hr : RequestAndEntitiesMatchEnvironment env request entities)
   (ht : typeOf (e.getAttr a) c env = .ok (tx, c'))
-  (hl : TypedExpr.AtLevel tx n)
+  (hl : TypedExpr.AtLevel tx n nmax)
   (hel : ¬ TypedExpr.EntityLitViaPath tx path)
   (he : evaluate (e.getAttr a) request entities = .ok v)
   (ha : Value.EuidViaPath v path euid)
@@ -376,14 +376,13 @@ theorem checked_eval_entity_reachable_get_attr {e : Expr} {n : Nat} {c c' : Capa
   rw [htx] at hl
   have ⟨ hgc, v, he', hi ⟩ := type_of_is_sound hc hr ht'
   cases hl
-  case getAttr n hel hl hety  =>
+  case getAttr v₁' ety n hel hety hl =>
     have ⟨euid', hv⟩ : ∃ euid', v = Value.prim (Prim.entityUID euid') := by
       rw [hety] at hi
       have ⟨ euid', hety, hv⟩ := instance_of_entity_type_is_entity hi
       simp [hv]
     subst hv
 
-    rename_i v₁' _
     have hv : v₁' = Value.prim (Prim.entityUID euid') := by
       unfold EvaluatesTo at he'
       rw [he₁] at he'
@@ -494,7 +493,7 @@ theorem checked_eval_entity_reachable_record {rxs : List (Attr × Expr)} {n : Na
   (hc : CapabilitiesInvariant c request entities)
   (hr : RequestAndEntitiesMatchEnvironment env request entities)
   (ht : typeOf (.record rxs) c env = .ok (tx, c'))
-  (hl : TypedExpr.AtLevel tx n)
+  (hl : TypedExpr.AtLevel tx n nmax)
   (hel : ¬ TypedExpr.EntityLitViaPath tx path)
   (he : evaluate (.record rxs) request entities = .ok v)
   (ha : Value.EuidViaPath v path euid)
@@ -533,7 +532,7 @@ theorem checked_eval_entity_reachable_record {rxs : List (Attr × Expr)} {n : Na
   simp only [Prod.mk.injEq, true_and, exists_and_left] at het
   replace ⟨_, het ⟩ := het
 
-  have hl' : TypedExpr.AtLevel atx n := by
+  have hl' : TypedExpr.AtLevel atx n nmax := by
     cases hl
     rename_i hl
     exact hl (a, atx) (Map.make_mem_list_mem (Map.find?_mem_toList hfatx))
@@ -564,11 +563,11 @@ theorem call_not_euid_via_path {xfn : ExtFun} {xs : List Expr} {entities : Entit
 If an expression checks at level `n` and then evaluates an entity (or a record
 containing an entity), then that entity must reachable in `n + 1` steps.
 -/
-theorem checked_eval_entity_reachable {e : Expr} {n : Nat} {c c' : Capabilities} {tx : TypedExpr} {env : Environment} {request : Request} {entities : Entities} {v : Value} {path : List Attr} {euid : EntityUID}
+theorem checked_eval_entity_reachable {e : Expr} {n nmax: Nat} {c c' : Capabilities} {tx : TypedExpr} {env : Environment} {request : Request} {entities : Entities} {v : Value} {path : List Attr} {euid : EntityUID}
   (hc : CapabilitiesInvariant c request entities)
   (hr : RequestAndEntitiesMatchEnvironment env request entities)
   (ht : typeOf e c env = .ok (tx, c'))
-  (hl : TypedExpr.AtLevel tx n)
+  (hl : TypedExpr.AtLevel tx n nmax)
   (hel : ¬ TypedExpr.EntityLitViaPath tx path)
   (he : evaluate e request entities = .ok v)
   (ha : Value.EuidViaPath v path euid)
@@ -701,7 +700,7 @@ theorem checked_eval_entity_in_slice  {n : Nat} {c c' : Capabilities} {tx : Type
   (hc : CapabilitiesInvariant c request entities)
   (hr : RequestAndEntitiesMatchEnvironment env request entities)
   (ht : typeOf e c env = .ok (tx, c'))
-  (hl : TypedExpr.AtLevel tx n)
+  (hl : TypedExpr.AtLevel tx n nmax)
   (hrt : ¬ TypedExpr.EntityLitViaPath tx [])
   (he : evaluate e request entities = .ok (Value.prim (Prim.entityUID euid)))
   (hf : entities.find? euid = some ed)
@@ -736,11 +735,11 @@ theorem not_entities_then_not_slice {n: Nat} {request : Request} {uid : EntityUI
   subst hs
   exact mapm_none_find_none hs₂ hse
 
-theorem checked_eval_entity_find_entities_eq_find_slice  {n : Nat} {c c' : Capabilities} {tx : TypedExpr} {env : Environment} {slice entities : Entities}
+theorem checked_eval_entity_find_entities_eq_find_slice  {n nmax : Nat} {c c' : Capabilities} {tx : TypedExpr} {env : Environment} {slice entities : Entities}
   (hc : CapabilitiesInvariant c request entities)
   (hr : RequestAndEntitiesMatchEnvironment env request entities)
   (ht : typeOf e c env = .ok (tx, c'))
-  (hl : TypedExpr.AtLevel tx n)
+  (hl : TypedExpr.AtLevel tx n nmax)
   (hrt : ¬ TypedExpr.EntityLitViaPath tx [])
   (he : evaluate e request entities = .ok (Value.prim (Prim.entityUID euid)))
   (hs : slice = Entities.sliceAtLevel entities request (n + 1)) :
diff --git a/cedar-lean/Cedar/Thm/Validation/Levels/UnaryApp.lean b/cedar-lean/Cedar/Thm/Validation/Levels/UnaryApp.lean
index 829a4224d..c5ee98064 100644
--- a/cedar-lean/Cedar/Thm/Validation/Levels/UnaryApp.lean
+++ b/cedar-lean/Cedar/Thm/Validation/Levels/UnaryApp.lean
@@ -33,11 +33,12 @@ open Cedar.Spec
 open Cedar.Validation
 
 theorem level_based_slicing_is_sound_unary_app {op : UnaryOp} {e : Expr} {n : Nat} {c₀ c₁: Capabilities} {env : Environment} {request : Request} {entities slice : Entities}
-  (hs : slice = entities.sliceAtLevel request n)
+  (hn : nmax ≥ n)
+  (hs : slice = entities.sliceAtLevel request nmax)
   (hc : CapabilitiesInvariant c₀ request entities)
   (hr : RequestAndEntitiesMatchEnvironment env request entities)
   (ht : typeOf (.unaryApp op e) c₀ env = Except.ok (tx, c₁))
-  (hl : TypedExpr.AtLevel tx n)
+  (hl : TypedExpr.AtLevel tx n nmax)
   (ihe : TypedAtLevelIsSound e)
   : evaluate (.unaryApp op e) request entities = evaluate (.unaryApp op e) request slice
 := by
@@ -45,5 +46,5 @@ theorem level_based_slicing_is_sound_unary_app {op : UnaryOp} {e : Expr} {n : Na
   subst tx
   cases hl
   rename_i hl₁
-  specialize ihe hs hc hr htx₁ hl₁
+  specialize ihe hn hs hc hr htx₁ hl₁
   simp [evaluate, ihe]
diff --git a/cedar-lean/Cedar/Validation/Levels.lean b/cedar-lean/Cedar/Validation/Levels.lean
index 9f1b56457..422744a69 100644
--- a/cedar-lean/Cedar/Validation/Levels.lean
+++ b/cedar-lean/Cedar/Validation/Levels.lean
@@ -57,50 +57,50 @@ where
     | _, _ => true
   termination_by tx
 
-def checkLevel (tx : TypedExpr) (n : Nat) : Bool :=
+def checkLevel (tx : TypedExpr) (l lmax : Nat) : Bool :=
   match tx with
   | .lit _ _ => true
   | .var _ _ => true
   | .ite x₁ x₂ x₃ _ =>
-    checkLevel x₁ n &&
-    checkLevel x₂ n &&
-    checkLevel x₃ n
+    checkLevel x₁ lmax lmax &&
+    checkLevel x₂ l lmax &&
+    checkLevel x₃ l lmax
   | .unaryApp _ x₁ _ =>
-    checkLevel x₁ n
+    checkLevel x₁ l lmax
   | .binaryApp .mem x₁ x₂ _
   | .binaryApp .getTag x₁ x₂ _
   | .binaryApp .hasTag x₁ x₂ _ =>
     notEntityLit x₁ &&
-    n > 0 &&
-    checkLevel x₁ (n - 1) &&
-    checkLevel x₂ n
+    l > 0 &&
+    checkLevel x₁ (l - 1) lmax &&
+    checkLevel x₂ lmax lmax
   | .and x₁ x₂ _
   | .or x₁ x₂ _
   | .binaryApp _ x₁ x₂ _ =>
-    checkLevel x₁ n &&
-    checkLevel x₂ n
+    checkLevel x₁ l lmax &&
+    checkLevel x₂ l lmax
   | .hasAttr x₁ _ _
   | .getAttr x₁ _ _ =>
     match x₁.typeOf with
     | .entity _ =>
       notEntityLit x₁ &&
-      n > 0 &&
-      checkLevel x₁ (n - 1)
-    | _ => checkLevel x₁ n
+      l > 0 &&
+      checkLevel x₁ (l - 1) lmax
+    | _ => checkLevel x₁ l lmax
   | .call _ xs _
   | .set xs _ =>
     xs.attach.all λ e =>
       have := List.sizeOf_lt_of_mem e.property
-      checkLevel e n
+      checkLevel e l lmax
   | .record axs _ =>
     axs.attach.all λ e =>
       have : sizeOf e.val.snd < 1 + sizeOf axs := by
         have h₁ := List.sizeOf_lt_of_mem e.property
         rw [Prod.mk.sizeOf_spec e.val.fst e.val.snd] at h₁
         omega
-      checkLevel e.val.snd n
+      checkLevel e.val.snd l lmax
 
 def typecheckAtLevel (policy : Policy) (env : Environment) (n : Nat) : Bool :=
   match typeOf policy.toExpr ∅ env with
-  | .ok (tx, _) => checkLevel tx n
+  | .ok (tx, _) => checkLevel tx n n
   | _           => false