Proved Nil case of itno_conserves_keys, and proved some helper lemmata.