CNF lifts INC through LAM:
But it does not lift INC through other constructors. For example:
should reduce to:
but currently doesn't.
Either INC lifting should be generalized to all node types, not just LAM, or LAM should not lift INCs.
This discrepancy is confusing