[Agda] question about termination checker

[selinger at mathstat.dal.ca]

Hello,

perhaps this is a dumb question, but it has stumped me. Why does the
termination checker accept lemma1, but not lemma2? Using Agda 2.6.0.1.

Thanks, -- Peter

data Nat : Set where
  zero : Nat
  succ : Nat -> Nat

lemma1 : Nat -> Nat
lemma1 zero = zero
lemma1 (succ zero) = zero
lemma1 (succ (succ x)) = lemma1 (succ x)

lemma2 : Nat -> Nat
lemma2 zero = zero
lemma2 (succ zero) = zero
lemma2 (succ (succ x)) = ih
  where
  ih = lemma2 (succ x)