Reindent Tarski
lemma 4, fix patch