finish proof that new_type_definition preserves consistency