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.