% References cited in https://agora.t9k.dev/t/240/weak-normalization-implies-strong-normalization-in-pure-type-systems