| he::tl -> whdaux tl (S.subst he t)
(* when name is Anonimous the substitution should be superfluous *)
)
+ | C.LetIn (n,s,t) -> whdaux l (S.subst (whdaux [] s) t)
| C.Appl (he::tl) -> whdaux (tl@l) he
| C.Appl [] -> raise (Impossible 1)
| C.Const (uri,cookingsno) as t ->