[ bugfix ] Missing bifunctor instance + plus def

* Bifunctor was not defined for Tm
* plus is now properly defined on the natural numbers. The whole
  induction principle takes a bit of getting used to but it works.