| Cic.Implicit _ -> assert false
| Cic.Cast (t1,t2) -> guess_a_name context t1
| Cic.Prod (na_,_,t) -> higher_name 1 t
- | Cic.Lambda _ -> assert false
- | Cic.LetIn (_,s,t) -> guess_a_name context (CicSubstitution.subst s t)
+(* warning: on appl we should beta reduce before the recursive call
+ | Cic.Lambda _ -> assert false
+*)
+ | Cic.LetIn (_,s,t) -> guess_a_name context (CicSubstitution.subst ~avoid_beta_redexes:true s t)
| Cic.Appl [] -> assert false
| Cic.Appl (he::_) -> guess_a_name context he
| Cic.Const (uri,_)