| Cic.Cast (te,ty) -> Cic.Cast (aux k te, aux k ty)
| Cic.Prod (n,s,t) -> Cic.Prod (n, aux k s, aux (k+1) t)
| Cic.Lambda (n,s,t) -> Cic.Lambda (n, aux k s, aux (k+1) t)
- | Cic.LetIn (n,s,t) -> Cic.LetIn (n, aux k s, aux (k+1) t)
+ | Cic.LetIn (n,s,ty,t) -> Cic.LetIn (n, aux k s, aux k ty, aux (k+1) t)
| Cic.Appl [] -> assert false
| Cic.Appl l -> Cic.Appl (List.map (aux k) l)
| Cic.Const (uri,exp_named_subst) ->