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