Strong Normalization is also an important property, which guarantees that
no typed term has an infinite reduction sequence.
Following standard proofs (see, e.g., [1]}), we prove this theorem by translating \(\lambda ^{\textrm {MD}}\)  to the simply typed lambda calculus.
