Break dependency of algebra on base_logic

Currently, parts of algebra depend on base_logic for the "internalized" equality and validity lemmas. That is rather annoying as it means many things need to be recompiled to work on those parts of algebra. It also prevents us from separating the base_logic and program_logic folders into a separate package, should we ever want to do that.

The plan is to instead add a file like base_logic/algebra.v and prove those lemmas there, thus fixing the dependency inversion.