Theorem: KolmogorovStreams.break_into_words_cons (Compfiles/KolmogorovStreams.lean)

State before:
α : Type
lengths : Stream' ℕ
first_length : ℕ
a : Stream' α
⊢ (break_into_words (first_length :: lengths) a).tail = break_into_words lengths (Stream'.drop first_length a)
Tactic:
simp [break_into_words, Stream'.corec, Stream'.tail_map, Stream'.tail_iterate]
State after:
no goals