# 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)