theorem Cedar.Thm.partial_evaluate_is_sound_or {x₁ x₂ : Spec.Residual} {req : Spec.Request} {es : Spec.Entities} {preq : TPE.PartialRequest} {pes : TPE.PartialEntities} {env : Validation.TypeEnv} (h₂ : InstanceOfWellFormedEnvironment req es env) (h₃ : RequestAndEntitiesRefine req es preq pes) (hᵢ₁ : Residual.WellTyped env x₁) (hᵢ₂ : Residual.WellTyped env x₂) (hᵢ₃ : x₁.typeOf = Validation.CedarType.bool Validation.BoolType.anyBool) (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)) : Except.toOption ((x₁.or x₂ (Validation.CedarType.bool Validation.BoolType.anyBool)).evaluate req es) = Except.toOption ((TPE.evaluate (x₁.or x₂ (Validation.CedarType.bool Validation.BoolType.anyBool)) preq pes).evaluate req es)