convert_to ((Stream'.corec (λ x ↦ Stream'.take (x.fst.head) x.snd)
               (λ x ↦ ⟨x.fst.tail, Stream'.drop (x.fst.head) x.snd⟩)) :
                Stream' ℕ × Stream' α → Stream' (List α)) ⟨lengths, a⟩ n =
           Stream'.take (lengths n) (Stream'.drop (∑ j in Finset.range n, lengths j) a)
case h
α : Type
lengths : Stream' ℕ
a : Stream' α
n : ℕ
⊢ break_into_words lengths a n = Stream'.take (lengths n) (Stream'.drop (∑ j ∈ Finset.range n, lengths j) a)
case h
α : Type
lengths : Stream' ℕ
a : Stream' α
n : ℕ
⊢ Stream'.corec (fun x => Stream'.take x.1.head x.2) (fun x => (x.1.tail, Stream'.drop x.1.head x.2)) (lengths, a) n =
    Stream'.take (lengths n) (Stream'.drop (∑ j ∈ Finset.range n, lengths j) a)