| C.Prod (n,s,t) -> C.Prod (n, aux s, aux t)
| C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t)
| C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t)
- | C.Appl l -> C.Appl (List.map aux l)
+ | C.Appl l ->
+ (* Invariant enforced: no application of an application *)
+ (match List.map aux l with
+ (C.Appl l')::tl -> C.Appl (l'@tl)
+ | l' -> C.Appl l')
| C.Const _ as t -> t
| C.Abst _ as t -> t
| C.MutInd _ as t -> t