module TerminationTwoConstructors where

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

bla : Nat -> Nat
bla m = m

f : Nat -> Nat
f zero = zero
f (suc zero) = zero
f (suc (suc n)) with bla (suc (suc n))
... | m = f (suc n)