theorem Cedar.Thm.partial_evaluate_is_sound_unary_app {x₁ : Spec.Residual} {req : Spec.Request} {es : Spec.Entities} {preq : TPE.PartialRequest} {pes : TPE.PartialEntities} {op₁ : Spec.UnaryOp} {ty : Validation.CedarType} (hᵢ₁ : Except.toOption (x₁.evaluate req es) = Except.toOption ((TPE.evaluate x₁ preq pes).evaluate req es)) : Except.toOption ((Spec.Residual.unaryApp op₁ x₁ ty).evaluate req es) = Except.toOption ((TPE.evaluate (Spec.Residual.unaryApp op₁ x₁ ty) preq pes).evaluate req es)