consistent naming of sort
more renaming of sort
equip witnesses with typing info
changed notation for operations