theorem
Cedar.Thm.level_based_slicing_is_sound_call
{xfn : Spec.ExtFun}
{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.call xfn 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.call xfn xs) request entities = Spec.evaluate (Spec.Expr.call xfn xs) request (entities.sliceAtLevel request n)