theorem Cedar.Thm.partial_evaluate_is_sound_set {req : Spec.Request} {es : Spec.Entities} {preq : TPE.PartialRequest} {pes : TPE.PartialEntities} {ls : List Spec.Residual} {ty : Validation.CedarType} (hᵢ₁ : ∀ (x : Spec.Residual), x ∈ ls → Except.toOption (x.evaluate req es) = Except.toOption ((TPE.evaluate x preq pes).evaluate req es)) : Except.toOption ((Spec.Residual.set ls ty.set).evaluate req es) = Except.toOption ((TPE.evaluate (Spec.Residual.set ls ty.set) preq pes).evaluate req es)