simp only [head, nth, drop, zero_add]
case hf.mk.intro.refl.refl
α✝ : Type u_1
σ : Stream' α✝
i : ℕ
⊢ (match (drop (i + i / 2) σ, (i + 1) % 2) with
    | (σ, snd) => head σ) =
    σ (i + i / 2)
no goals