theorem Cedar.Thm.partial_eval_well_typed_hasAttr {env : Validation.TypeEnv} {expr : Spec.Residual} {attr : Spec.Attr} {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 (expr.hasAttr attr ty) (TPE.evaluate (expr.hasAttr attr ty) preq pes) req preq es pes