Normalize variable declarations

We no longer need to separate [Variable foo : PreCategory] onto multiple
lines to separate universes.

This change made by invoking

    git ls-files '*.v' | xargs python combine_variables.py

on

```python
#!/usr/bin/env python
from __future__ import with_statement
import re, sys

REG = re.compile(r'^(\s*)Variables?\s+([^:]+):([^\.]+)\.\s*$')
def groups_to_string(indent, variables, types):
    variable_list = [i for i in variables.split(' ') if i]
    var = ('Variables' if len(variable_list) > 1 else 'Variable')
    return '%s%s %s : %s.' % (indent,
                              var,
                              ' '.join(variable_list),
                              types.strip())
def fix_file(contents):
    ret = []
    prev_groups = tuple()
    for line in contents.split('\n'):
        next_groups = REG.findall(line)
        if prev_groups:
            indent, variables, types = prev_groups
            if next_groups:
                new_indent, new_variables, new_types = next_groups[0]
                if new_indent == indent and types.strip() == new_types.strip():
                    prev_groups = (indent, variables + ' ' + new_variables, types)
                else:
                    ret.append(groups_to_string(indent, variables, types))
                    prev_groups = (new_indent, new_variables, new_types)
            else:
                ret.append(groups_to_string(indent, variables, types))
                ret.append(line)
                prev_groups = tuple()
        elif next_groups:
            prev_groups = next_groups[0]
        else:
            ret.append(line)
    if prev_groups:
        ret.append(groups_to_string(*prev_groups))
    return '\n'.join(ret)

if __name__ == '__main__':
    if len(sys.argv) == 1 or '--help' in sys.argv or '-h' in sys.argv:
        print('Usage: %s FILE_NAME [FILE_NAME ..]' % sys.argv[0])
        print('Replaces [Variable X : T. Variable Y : T.] with [Variables X Y : T.]')
        sys.exit(0)
    for i in sys.argv[1:]:
        with open(i, 'r') as f:
            contents = f.read()
        new_contents = fix_file(contents)
        if new_contents != contents:
            with open(i, 'w') as f:
                f.write(new_contents)
```
Merge pull request #632 from JasonGross/combine-variables

Normalize variable declarations
Splitting of coherent idempotents
A counterexample: not every idempotent is coherent
fix nits in Idempotent.v
Merge pull request #635 from mikeshulman/idempotents

Splitting of coherent idempotents