fix hardcoded bottoms
emit prog on top level, rather than at the end of each class definition
fewer debug output, umn
fewer debug print, not recording proof directly (different design)
initial cleanup after removal