rec_check.ml: high-level documentation and reordering

We provide an ocamldoc-style module comment to explain the general
lines of the recursive check. This complements existing comments about
the term- and binding-judgments that are more implementation-oriented.

It was natural to reorder the code so that the "static or dynamic
size" code is apart from the "usage of recursive variables" code.

Finally, I also added copyright headers to reflect the now shared
authorship of the code. (Alban has signed a CLA.)