switch end of proof step marker from ".." to ";;"
change notation a bit
change notation a bit
update
remove a non-optimization