[examples/lambda] Establish new type of λ-terms, with constants

This is isomorphic to the original Gordon-Melham type (see
other-models/ncScript.sml), where we have the traditional three
constructors as well as an extra CONST constructor that injects values
from α.

The construction here exercises the "generic" term machinery (and
forces a tweak to one of its few bits of automation).