knuton/la-girafe-sportive — pull request #12 by yfyf (2013-12-13 01:17:18+00:00)
Title: Proof that eta is substitutive

Uhm, see my comments / try following the proof. You might bump into something likes this too.

Also, I think the notation hack needs to be improved, because it only looks good for closed terms, elsewhere you get things like this:

```coq
((fix subst (v : nat) (r t : lterm) {struct t} : lterm :=
match t with
| ​i =>
match Compare_dec.nat_compare i v with
| Eq => lift v 0 r
| Lt => ​i
| Gt => ​(i - 1)
end
| λ m => λ subst (v + 1) r m
| m n0 => subst v r m subst v r n0
end) (n + 1) L x)
```
i.e. it becomes impossible to distinguish terms and variables.