theorem Cedar.Thm.level_based_slicing_is_sound_set {tx : Validation.TypedExpr} {xs : List Spec.Expr} {n : Nat} {c₀ c₁ : Validation.Capabilities} {env : Validation.TypeEnv} {request : Spec.Request} {entities : Spec.Entities} (hc : CapabilitiesInvariant c₀ request entities) (hr : InstanceOfWellFormedEnvironment request entities env) (ht : Validation.typeOf (Spec.Expr.set xs) c₀ env = Except.ok (tx, c₁)) (hl : Validation.TypedExpr.AtLevel env tx n) (ih : ∀ (x : Spec.Expr), x ∈ xs → TypedAtLevelIsSound x) : Spec.evaluate (Spec.Expr.set xs) request entities = Spec.evaluate (Spec.Expr.set xs) request (entities.sliceAtLevel request n)