theorem Cedar.Thm.partial_eval_well_typed_set {env : Validation.TypeEnv} {ls : List Spec.Residual} {ty : Validation.CedarType} {req : Spec.Request} {preq : TPE.PartialRequest} {es : Spec.Entities} {pes : TPE.PartialEntities} : (∀ (r : Spec.Residual), r ∈ ls → Residual.WellTyped env (TPE.evaluate r preq pes)) → PEWellTyped env (Spec.Residual.set ls ty) (TPE.evaluate (Spec.Residual.set ls ty) preq pes) req preq es pes

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