Filled in some of the details for lemmas about multi-step reductions
Filled in some of the details for lemmas about multi-step reductions

andreasabel/strong-normalization,andreasabel/strong-normalization