The `spiral` function: a perplexing piece of coinduction

Spiral.hs

module Spiral where

-- Based on <pigworker.wordpress.com/2015/01/02/coinduction>

data Tree x = Leaf x
            | Branch x (Tree x) (Tree x)
            deriving ( Show )

data Stream x = x :> Stream x
              deriving ( Show )

spiral :: (Stream a -> (b, Stream a)) -> a -> b
spiral f a =
   b where (b, as) = f (a :> as)

label :: Tree () -> Tree Integer
label tree = spiral (help tree) 0

help :: Tree () -> Stream Integer -> (Tree Integer, Stream Integer)
help t (i :> is0) = case t of
   Leaf () ->
      (Leaf i, (i + 1) :> is0)
   Branch () lt rt ->
      let (lt', is1) = help lt is0
          (rt', is2) = help rt is1
      in (Branch i lt' rt', (i + 1) :> is2)