theorem Cedar.Thm.partial_evaluate_is_sound_get_attr {x₁ : Spec.Residual} {req : Spec.Request} {es : Spec.Entities} {preq : TPE.PartialRequest} {pes : TPE.PartialEntities} {attr : Spec.Attr} {ty : Validation.CedarType} (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₁.getAttr attr ty).evaluate req es) = Except.toOption ((TPE.evaluate (x₁.getAttr attr ty) preq pes).evaluate req es)