if does_not_occur 1 t_typ then
(* since [Rel 1] does not occur in typ, substituting any term *)
(* in place of [Rel 1] is equivalent to delifting once *)
- CicSubstitution.subst (C.Implicit None) t_typ)
+ CicSubstitution.subst (C.Implicit None) t_typ
else
C.LetIn (n,s,ty,t_typ)
| C.Appl (he::tl) when List.length tl > 0 ->