add implementation notes on TTS: TTS-internal-witnesses.tex
fix a misprint
change end of proof step marker to ".."