Added contractible singletons (hopefully correct).

Uncommented J and lemId now typechecks.