theorem Cedar.Thm.partial_evaluate_is_sound_ext_has_attr {env : Validation.TypeEnv} {x₁ : Spec.Residual} {req : Spec.Request} {es : Spec.Entities} {preq : TPE.PartialRequest} {pes : TPE.PartialEntities} {attr : Spec.Attr} {attrs : List Spec.Attr} (hwf : InstanceOfWellFormedEnvironment req es env) (hwt : Residual.WellTyped env x₁) (h₄ : RequestAndEntitiesRefine req es preq pes) (hᵢ₁ : Except.toOption (x₁.evaluate req es) = Except.toOption ((TPE.evaluate env x₁ preq pes).evaluate req es)) : Except.toOption ((x₁.extHasAttr attr attrs (Validation.CedarType.bool Validation.BoolType.anyBool)).evaluate req es) = Except.toOption ((TPE.evaluate env (x₁.extHasAttr attr attrs (Validation.CedarType.bool Validation.BoolType.anyBool)) preq pes).evaluate req es)