  where
    walk c t'@(TmVar _ x) 
      | x == j + c = shift c s
      | otherwise = t'
    walk c (TmApp ifo t1 t2) = TmApp ifo (walk c t1) (walk c t2)
    walk c (TmAbs ifo x t1) = TmAbs ifo x (walk (c+1) t1)

isValue :: Term -> Bool
isValue (TmAbs _ _ _) = True
isValue (TmVar _ _) = True
isValue _ = False