andrejbauer/tt — pull request #21 by JasonGross (2014-05-21 19:30:57+00:00)
Title: 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`.)