theorem Cedar.Thm.partial_evaluate_is_sound_ite {x₁ x₂ x₃ : Spec.Residual} {req : Spec.Request} {es : Spec.Entities} {preq : TPE.PartialRequest} {pes : TPE.PartialEntities} {env : Validation.TypeEnv} (h₂ : InstanceOfWellFormedEnvironment req es env) (hwt : Residual.WellTyped env x₁) (hₜ : x₁.typeOf = Validation.CedarType.bool Validation.BoolType.anyBool) (hᵢ₁ : Except.toOption (x₁.evaluate req es) = Except.toOption ((TPE.evaluate x₁ preq pes).evaluate req es)) (hᵢ₂ : Except.toOption (x₂.evaluate req es) = Except.toOption ((TPE.evaluate x₂ preq pes).evaluate req es)) (hᵢ₃ : Except.toOption (x₃.evaluate req es) = Except.toOption ((TPE.evaluate x₃ preq pes).evaluate req es)) : Except.toOption ((x₁.ite x₂ x₃ x₂.typeOf).evaluate req es) = Except.toOption ((TPE.evaluate (x₁.ite x₂ x₃ x₂.typeOf) preq pes).evaluate req es)