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