remove algebra/ dependency on base_logic/

Move the uPred lemmas that reflect algebra properties into a file in the base_logic module, so that base_logic is now properly layered on top of {algebra, proofmode, bi}. In fact with this MR, algebra does not depend on proofmode or bi either, it is a proper lowest layer in the repository. (But this will likely change when we use siProp for real.)

Overall, the dependency stack should now look like this (with imports only within a block and from lower blocks):

heap_lang
program_logic
base_logic      si_logic
    {proofmode, bi}
        algebra

To be more precise, proofmode is imported in bi.lib but not in the bi root. So we could say {proofmode, bi} decomposes into

bi.lib
proofmode
bi root

Fixes #355 (closed)