Added proof saving and updated thunking to save state independent of proof system for easy saving; fixed some proof switching bugs in insertion mode