-- Works
total
life : Nat -> Nat
life (S (S x)) = life x
life _ = 42

-- Works
total
life : Nat -> Nat
life k = case k of
           (S (S y)) => life y
           _         => 42

-- Main.life is possibly not total due to recursive path Main.life --> Main.life
total
life : Nat -> Nat
life (S x) = case x of
               (S y) => life y
               _     => 42
life _ = 42