Include useful redundant data in modalities

This adds to a `ReflectiveSubuniverse` the data of a predicate to be in the subuniverse, and to `Modality` the data of a general induction principle into modal types.  These can be defined, up to equivalence, from the data that used to be there, but in some examples (like `Truncation`) one or both of these data occur naturally in a way that is judgmentally different from (and better than) the one that can be constructed from the other data.  So I think it's better to include them as extra redundant data, with "easy" constructors that fill them in automatically if desired.  In particular, this fixes the problem Jason noticed in Freudenthal.  I think this is analogous to our choice to define `IsEquiv` using half-adjoint equivalences rather than, say, contractible fibers, so that the inverse function would be remembered as explicit data.
0. It lets you error early rather than late; in general (especially for `Qed`ed theorems), it's ok to change the proofs; if the theorems stay the same, you don't have to put as much effort into checking the proof changes.  But without `using`, changing the proof in a seemingly innocuous way can change what theorem you're proving.
1. It lets you control how many arguments your theorem takes, which you're otherwise letting Coq infer.
2. It makes it so that the unnamed arguments don't show up if you use `abstract`
3. I think it lets the parallel machinery work a bit better (or, perhaps, at all?) in `Qed`ed proofs