Desired property normal form implies values

A desirable property of a Lambda calculus where there's no Stuck term. This property may not hold in most systems.