Weak normalization theorem for simply typed lambda calculus
= Weak normalization theorem for simply typed lambda calculus
{c}
Every well-typed term in the simply typed lambda calculus has some finite beta-reduction sequence ending in a beta-normal form.