Strong normalization theorem for simply typed lambda calculus
= Strong normalization theorem for simply typed lambda calculus
{c}
{wiki=Normalization_property_(abstract_rewriting)#Strong_normalization}
Every well-typed simply typed lambda term admits no infinite beta-reduction sequence.