theorem
Cedar.Thm.partial_eval_well_typed_var
{env : Validation.TypeEnv}
{v : Spec.Var}
{ty : Validation.CedarType}
{req : Spec.Request}
{preq : TPE.PartialRequest}
{es : Spec.Entities}
{pes : TPE.PartialEntities}
:
PEWellTyped env (Spec.Residual.var v ty) (TPE.evaluate (Spec.Residual.var v ty) preq pes) req preq es pes