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)
| NCic.Lambda (n,s,t) as orig ->
let s1 = f k s in let t1 = f (g (n,NCic.Decl s) k) t in