Add invariants to itno2_induct.
Duplicate many lemmata about nog for nog2.
Use nog2 etc. everywhere.