Moving to Program Instances for examples, renamed iHammer to iSmash, empty_hyps are now removed on introduction.

Separated int_as_nat_diff library, extra pure hints no longer need ugly ltac overriding, improved spin and ticket lock allocation specs.

Can now iInv on SolveSep goal, minor changes, improved table generation function to incorporate data about other tools' examples.