Strong normalization theorem for simply typed lambda calculus

ID: strong-normalization-theorem-for-simply-typed-lambda-calculus

Every well-typed simply typed lambda term admits no infinite beta-reduction sequence.

New to topics? Read the docs here!