A simple coinductive proof

cotest.idr

  ones : Num a => Stream a
  ones = 1 :: ones
  
  twos : Num a => Stream a
  twos = 2 :: twos
  
  codata EqStream : Stream a -> Stream a -> Type where
    ReflStream : x = y -> EqStream xs ys -> EqStream (x :: xs) (y :: ys)
  
  -- can't do it for all Num since we don't know how * behaves!
  p : EqStream (map (*2) (ones {a=Int})) twos
  p = ReflStream refl p