Uniformize reflective subuniverses and modalities

And also add a few more examples.  This closes #457.  The use of typeclasses is a bit hackish (see comments in `ReflectiveSubuniverse.v`), but it's the best way I've been able to think of to avoid having to pass the modality as an argument to everything all the time when there is only one modality hanging around.
Possibilities that come to mind immediately:
- `moveRE_V`
- `moveR_E_V`
- `moveR_V_E`
- `moveR_E__V`
- `moveR_V__E`
- `moveER_V`
- `emove_V`
- `Emove_V`

In all of these, there'd only ever be one `E` (and it would be separate, so I'd be less likely to read it and be confused about what thing we're moving), but the `V` could be extended.  Some of these might cause issues with things like `p_Vp`.