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