A simple rewrite proof of the equational interpolation theorem
As the title says