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

theorem Cedar.Thm.level_based_slicing_is_sound_if {tx : Validation.TypedExpr} {x₁ x₂ x₃ : 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) (htx : Validation.typeOf (x₁.ite x₂ x₃) c₀ env = Except.ok (tx, c₁)) (hl : Validation.TypedExpr.AtLevel env tx n) (ih₁ : TypedAtLevelIsSound x₁) (ih₂ : TypedAtLevelIsSound x₂) (ih₃ : TypedAtLevelIsSound x₃) : Spec.evaluate (x₁.ite x₂ x₃) request entities = Spec.evaluate (x₁.ite x₂ x₃) request (entities.sliceAtLevel request n)