| C.Prod (n,s,t) -> C.Prod (n, substaux k s, substaux (k + 1) t)
| C.Lambda (n,s,t) -> C.Lambda (n, substaux k s, substaux (k + 1) t)
| C.LetIn (n,s,t) -> C.LetIn (n, substaux k s, substaux (k + 1) t)
| C.Prod (n,s,t) -> C.Prod (n, substaux k s, substaux (k + 1) t)
| C.Lambda (n,s,t) -> C.Lambda (n, substaux k s, substaux (k + 1) t)
| C.LetIn (n,s,t) -> C.LetIn (n, substaux k s, substaux (k + 1) t)