theorem Cedar.Thm.partial_evaluate_is_sound_binary_app {op₂ : Spec.BinaryOp} {ty : Validation.CedarType} {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) (hwt : Residual.WellTyped env x₂) (howt : Spec.BinaryResidualWellTyped env op₂ x₁ x₂ ty) (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 ((Spec.Residual.binaryApp op₂ x₁ x₂ ty).evaluate req es) = Except.toOption ((TPE.evaluate (Spec.Residual.binaryApp op₂ x₁ x₂ ty) preq pes).evaluate req es)