A bunch of work towards proving logical equiv contains defintional.
Finish proving that logical equivalence contains definitional (modulo a lemma about substituting!)
Prove the lemma we needed for that last theorem. Wound up being easy.