- C.LetIn (n, beta_reduce s, beta_reduce ty, beta_reduce t)
+ let t' = beta_reduce ~clean t in
+ if clean && does_not_occur 1 t' 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'
+ else
+ C.LetIn (n, beta_reduce ~clean s, beta_reduce ~clean ty, t')