Explore getting rid of implication

It seems possible that we don't actually need implication and could work without it (so we'd work in intuitionistic linear logic instead of the more general separation logic/BI). Seems at least interesting to figure out of that's true. We could remove implication from the MoSeL interface and see what happens.

For Iris itself I mostly expect this to work, but the general linear case might make this harder. Or not.