theorem Cedar.Thm.partial_evaluate_is_sound_error {req : Spec.Request} {es : Spec.Entities} {preq : TPE.PartialRequest} {pes : TPE.PartialEntities} {ty : Validation.CedarType} : Except.toOption ((Spec.Residual.error ty).evaluate req es) = Except.toOption ((TPE.evaluate (Spec.Residual.error ty) preq pes).evaluate req es)

theorem Cedar.Thm.partial_evaluate_is_sound {x : Spec.Residual} {req : Spec.Request} {es : Spec.Entities} {preq : TPE.PartialRequest} {pes : TPE.PartialEntities} {env : Validation.TypeEnv} : Residual.WellTyped env x → InstanceOfWellFormedEnvironment req es env → RequestAndEntitiesRefine req es preq pes → Except.toOption (x.evaluate req es) = Except.toOption ((TPE.evaluate x preq pes).evaluate req es)

The main lemma: Evaluating a residual derived from partially evaluating a well-typed expression is equivalent to that of evaluating the original expression, provided that requests and entities are consistent. The equivalency is defined using Except.toOption.