Prove the eta rule for sigmas from a more general prinicple

Also, rename it to half_eta, because it says
  match u as u' return P u' with
    | (a; b) => (a; b)
  end
  ==
  u
rather than
  (match u as u' return A with
     | (a; b) => a
   end;
   match u as u' return P (match u' with (a; b) => a end) with
     | (a; b) => b
   end)
  ==
  u
which is the proper eta rule.  (More concisely, this is (u.1; u.2) == u.)
Jason's pull requests.
Merge branch 'master' of https://github.com/andrejbauer/tt
equal_whnf_ty wasn't being called! 2x speedup

Conflicts:
	brazil/equal.ml
Sped up debug printing of patterns, a lot
Alpha-equivalence respects magenta
Brazil/syntax.ml uses the mkZZZ fns
Optimize shifting by zero
typing.ml uses the mkZZZ fns
equal.ml uses mkZZZ, but not spines
Deleted remnants of spines from Pattern
3x speedup by a fail-fast in pattern-matching apps
Fixed ordering bug in desugaring of J type family
Better Input-to-string conversion
Fixed further J-ordering bugs
Exact pattern-matching up to standard equivalence
Also, slightly better debugging output
Prove sigma_eta and sigma_eta' (renamed to id_sigma)

Renamed sigma_eta' because it's classifying the strict identity type
of sigmas.

Unfortunately, sigma_eta is rather slow; on my machine:
$ time ./brazil.native examples/sigma.br
...
real    0m14.380s
user    0m14.281s
sys     0m0.047s
Add sigma.br to the brazil smoketest