| C.LetIn (n,s,t) -> CicSubstitution.subst (letin_nf s) t
| C.Appl l -> C.Appl (List.map letin_nf l)
| C.Const _ as t -> t
| C.LetIn (n,s,t) -> CicSubstitution.subst (letin_nf s) t
| C.Appl l -> C.Appl (List.map letin_nf l)
| C.Const _ as t -> t
| C.MutInd _ as t -> t
| C.MutConstruct _ as t -> t
| C.MutCase (sp,cookingsno,i,outt,t,pl) ->
| C.MutInd _ as t -> t
| C.MutConstruct _ as t -> t
| C.MutCase (sp,cookingsno,i,outt,t,pl) ->