rw [←take_append_drop_take]
α : Type u_1
σ : Stream' α
i : ℕ
⊢ take (i + 1) σ = List.concat (take i σ) (σ i)
α : Type u_1
σ : Stream' α
i : ℕ
⊢ take i σ ++ take 1 (drop i σ) = List.concat (take i σ) (σ i)