Почему этот редуктор лямбда-исчисления не уменьшает succ с 0 до 1?

data Term = Var Integer
          | Apply Term Term
          | Lambda Term
          deriving (Eq, Show)

sub :: Term -> Integer -> Term -> Term
sub e v r = case e of
    Var x -> if x == v then r else e
    Apply m1 m2 -> Apply (sub m1 v r) (sub m2 v r)
    Lambda t -> Lambda (sub t (v + 1) r)

beta :: Term -> Term
beta t = case t of
    Apply (Lambda e) e' -> sub e 0 e'
    otherwise -> t

eta :: Term -> Term
eta t = case t of
    Lambda (Apply f (Var 0)) -> f
    otherwise -> t

reduce :: Term -> Term
reduce t = if t == t'
    then t
    else reduce t'
  where t' = beta . eta $ t

Я попытался:

let zero = Lambda $ Lambda $ Var 0
let succ = Lambda $ Lambda $ Lambda $ Apply (Var 1) $ (Apply (Apply (Var 2) (Var 1)) (Var 0))
reduce (Apply succ zero)

В GHCi, но, похоже, он не дал мне выражения для одного (Lambda (Lambda (Apply (Var 1) (Var 0)) того, что я ищу. Вместо этого он дает мне:

Lambda (Lambda (Apply (Var 1) (Apply (Apply (Lambda (Lambda (Var 0))) (Var 1)) (Var 0))))

Переменные кодируются не по имени, а по тому, сколько лямбд нужно пройти наружу, чтобы получить параметр.