| C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty)
| C.Prod (n,s,t) -> C.Prod (n, deliftaux k s, deliftaux (k+1) t)
| C.Lambda (n,s,t) -> C.Lambda (n, deliftaux k s, deliftaux (k+1) t)
| C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty)
| C.Prod (n,s,t) -> C.Prod (n, deliftaux k s, deliftaux (k+1) t)
| C.Lambda (n,s,t) -> C.Lambda (n, deliftaux k s, deliftaux (k+1) t)