Restructure derived_laws of BI
Some changes in preparation of !881 (merged)
- Move pure lemmas down; that is already in !881 (merged)
- Move
Affine
/Absorbing
/Persistent
instances up to fix some of the TODOs there (and some other circular issues that I have in my extension of !881 (merged)).
This MR should not add/remove/change any lemma statements. I changed some proofs to make things work with the new order.