theorem Cedar.Thm.partial_eval_well_typed_unaryApp {env : Validation.TypeEnv} {op : Spec.UnaryOp} {expr : Spec.Residual} {ty : Validation.CedarType} {req : Spec.Request} {preq : TPE.PartialRequest} {es : Spec.Entities} {pes : TPE.PartialEntities} : Residual.WellTyped env (TPE.evaluate expr preq pes) → PEWellTyped env (Spec.Residual.unaryApp op expr ty) (TPE.evaluate (Spec.Residual.unaryApp op expr ty) preq pes) req preq es pes

Helper theorem: Partial evaluation preserves well-typedness for unary application residuals.