theorem Cedar.Thm.partial_evaluate_is_sound_has_attr {x₁ : Spec.Residual} {req : Spec.Request} {es : Spec.Entities} {preq : TPE.PartialRequest} {pes : TPE.PartialEntities} {attr : Spec.Attr} (h₄ : RequestAndEntitiesRefine req es preq pes) (hᵢ₁ : Except.toOption (x₁.evaluate req es) = Except.toOption ((TPE.evaluate x₁ preq pes).evaluate req es)) : Except.toOption ((x₁.hasAttr attr (Validation.CedarType.bool Validation.BoolType.anyBool)).evaluate req es) = Except.toOption ((TPE.evaluate (x₁.hasAttr attr (Validation.CedarType.bool Validation.BoolType.anyBool)) preq pes).evaluate req es)