Move counting insert and add to Makefile.
Clean up insert complexity proof.

Also remove uses of CpdtTactics.