theorem Cedar.Thm.try_decide_residual₁_is_bool {op₁ : Spec.UnaryOp} {r : Spec.Residual} {v : Spec.Value} (hdec : TPE.tryDecideResidual₁ op₁ r = some v) : ∃ (b : Bool), v = Spec.Value.prim (Spec.Prim.bool b)

The reductions only ever decide a boolean.

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 env expr preq pes) → PEWellTyped env (Spec.Residual.unaryApp op expr ty) (TPE.evaluate env (Spec.Residual.unaryApp op expr ty) preq pes) req preq es pes

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