This is also known as "The Fundamental Theorem of Stream Calculus" in stream calculus. Using coinduction for an (infinite) stream sigma, eg

    sigma(0)      = head(sigma)
    sigma'        = tail(sigma)
    (a ++ sigma)' = sigma