Generic logic

This is perhaps not optimally polished, but I'm putting it out here for feedback.  The idea is that a "logic" is essentially a modality, and we can define all the logical operations relative to "a logic", with PAT-logic and (-1)-logic as important special cases.  More description can be found in the comments.  I included LEM as an example of how to use this kind of generic logic; next up would be AC, which is potentially parametrized by 2 or 3 different modalities/logics.

I had to make a bunch of choices about how to implement it, and my only indication that they're the right ones is that nothing else I tried worked as well.  So I'm very open to suggestions, up to and including "this is a terrible idea".

One particular infelicity is that this change slows down the compilation of `V.v` by almost a factor of 3.  I don't have any idea why that might be, but if it's going to consistently do that whenever we make heavy use of `hexists` (which `V.v` is currently the only theory that does), then one might argue that this is not worth it.
Because, for instance, the notation `~` defined here is not the same as the `~` defined in `Overture`.  They happen to be judgmentally equal (by the trick that I played in the definition of `Logic`) in many cases (specifically, when `Empty` is modal) but not always, and even in the cases when they are, I sometimes had some difficulty convincing Coq of it.  So if someone is using the `~` from `Overture`, they might want to import the `hexists` notation without the `~` notation from `Logic.Notations`.

I admit this is not an ideal solution.  I tried to think of an alternative notation for `hnot`, to prevent the conflict, but failed (absent unicode).  Perhaps this is an indication that logic in a general modality is too general; I considered only allowing modalities containing `Empty` to be called "logics", but I think there are examples that it would be reasonable to call "logics" which don't satisfy this condition, e.g. a lex modality representing the "locally true" logic of a subtopos, or the strong-mono modality in a quasitopos.