Use modules for reflective subuniverses and modalities

This is option (4) at #596.  It's still a bit annoying, but I think it's made manageable by the technique of making the module types represent a _family_ of subuniverses or modalities.  The universe polymorphism is fiddly when defining particular examples, but once they are defined, it's basically invisible, which is how it should be.  Note that hardly any of the substantial code has to be modified; most of the changes are in the boilerplate.  There are a couple of minor anomalies that have to be worked around (still working on bug reports), but nothing too major.  Right now I think this is probably the way to go -- I don't even know how to do option (3) for lex modalities -- but I'd be interested in what others think.  I'm also very open to feedback on the best way to name and manage the modules; I proposed one possible convention, but I don't know that it's the best.
Do you want to fix this?  I imagine something like the following should work (untested):
```coq
Ltac count_arrows_in T :=
  match T with
    | forall x : ?A, @?f x => let ret := constr:(fun x : A => let fx := f x in
                                                              $(let fx' := fx in
                                                                let fx'' := (eval cbv beta in fx') in
                                                                let n := count_arrows fx'' in
                                                                exact n)$) in
                              let ret' := (eval cbv beta zeta in ret) in
                              match ret' with
                                | fun _ => ?n => constr:(S n)
                              end
    | _ => constr:0
  end.

Ltac count_arrows_in_goal :=
  let G := match goal with |- ?G => constr:G end in
  count_arrows_in G.

Ltac intros_and_specialize_n IH n :=
  idtac;
  let G := match goal with |- ?G => constr:G end in
  let n' := count_arrows_in_goal in
  let n0 := (eval compute in n) in
  lazymatch eval compute in n' with
    | n => idtac
    | S _ => let x := fresh in
             intro x; specialize (IH x);
             intros_and_specialize_n IH n0
    | 0 => fail "Internal Error: Introduced too many hypotheses on goal" G
  end.

Ltac simple_induction n IH :=
  generalize dependent n;
  let n0 := count_arrows_in_goal in
  let n1 := match n0 with S ?n1 => constr:n1 end in (* decrement to not count [n] as one of the variables *)
  fix IH 1;
  intros [];
  [ clear IH | intros_and_specialize_n IH n1.. ].
```