This file proves that level checking for .unaryApp expressions is sound.

theorem Cedar.Thm.level_based_slicing_is_sound_unary_app {tx : Validation.TypedExpr} {op : Spec.UnaryOp} {e : 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.unaryApp op e) c₀ env = Except.ok (tx, c₁)) (hl : Validation.TypedExpr.AtLevel env tx n) (ihe : TypedAtLevelIsSound e) : Spec.evaluate (Spec.Expr.unaryApp op e) request entities = Spec.evaluate (Spec.Expr.unaryApp op e) request (entities.sliceAtLevel request n)