Normalization by Evaluation for a version of Martin-Löf Type Theory with weak explicit substitutions.