work towards proving new_type_definition preserves consistency

remains to show that the two new axioms about the bijections are
satisfied by the interpretation i've set up