Added TODO to add consequences of P a strict subset of polyL.
Adds missing definitions.