Compatibility import for the main-theorem proof

The definitions and internal proof now share one API. This module remains as a compatibility import for downstream users of the original file layout.