HOL-ex.Normalization_by_Evaluation