The definitions of Part 2 are in NormalizerLean/Defs.lean, with those of all six parts. This file only imports them, so that Statements.lean, which imports this file, is unchanged since freezing.