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