Term transformation and proof (re)construction