+author: luzio
split theorems in separate files; progress on th9