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

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