prove the cheat
reprove up to and including INST_TYPE_correct
prove new_basic_definition_correct