andrejbauer/tt — pull request #25 by JasonGross (2014-05-25 05:29:49+00:00)
Title: Prove sigma_eta and sigma_eta' (renamed to id_sigma)

Renamed sigma_eta' to id_sigma 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