Clean up insert complexity proof.

Also remove uses of CpdtTactics.