| 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.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)