dfsf.idr

using (p : a -> Type)

  -- codata Stream a = (::) a (Stream a)

  data Eventually_s : Stream a -> Type where
    Ev_b : p x -> Eventually_s (x :: xs)
    Ev_r : p x -> Eventually_s xs -> Eventually_s (x :: xs)

  eventually_s_inv : Eventually_s s -> s = x :: s' -> p x -> Eventually_s s'
  eventually_s_inv r@(Ev_b y) prf px = ?what
  eventually_s_inv (Ev_r y z) Refl px = z