chore(PFunctor): drop simp tags from non-universe generic bind lemma

[dtumad]

Currently PFunctor.FreeM.bind mx my is marked to simp to mx >>= my, but the notational Bind.bind only applies in cases where the return types of both monadic computation has the same universe level. This means other simp lemmas need to be written in both forms in order to provide full coverage.

This PR drops this tag, and a similar tag on FreeM.pure. It does not create a simp pathway in the other direction, but that could be worth considering I think.

[eric-wieser]

This effectively reverts #417. We have to choose between:

• status quo: lemmas about >>= have to be restated for .bind for universe polymorphism
• reverse simp lemmas: none of the wp or LawfulMonad machinery works out of the box