theorem Cedar.Thm.partial_evaluate_is_sound_record {m : List (Spec.Attr × Spec.Residual)} {rty : Validation.RecordType} {req : Spec.Request} {es : Spec.Entities} {preq : TPE.PartialRequest} {pes : TPE.PartialEntities} (hᵢ₁ : ∀ (k : Spec.Attr) (v : Spec.Residual), (k, v) ∈ m → Except.toOption (v.evaluate req es) = Except.toOption ((TPE.evaluate v preq pes).evaluate req es)) : Except.toOption ((Spec.Residual.record m (Validation.CedarType.record rty)).evaluate req es) = Except.toOption ((TPE.evaluate (Spec.Residual.record m (Validation.CedarType.record rty)) preq pes).evaluate req es)