if t1 == t && s1 == s then orig else NCic.Prod (n,s1,t1)
| NCic.Lambda (n,s,t) as orig ->
let s1 = f k s in let t1 = f (g (n,NCic.Decl s) k) t in
- if t1 == t && s1 == s then orig else NCic.Prod (n,s1,t1)
+ if t1 == t && s1 == s then orig else NCic.Lambda (n,s1,t1)
| NCic.LetIn (n,ty,t,b) as orig ->
let ty1 = f k ty in let t1 = f k t in
let b1 = f (g (n,NCic.Def (t,ty)) k) b in