congr
case h.e_a.succ
α : Type
pn : ℕ
hpn :
  ∀ (lengths : Stream' ℕ) (a : Stream' α),
    ((Stream'.iterate (fun x => (x.1.tail, Stream'.drop x.1.head x.2)) (lengths, a)).get pn).2 =
      Stream'.drop (∑ j ∈ Finset.range pn, lengths j) a
a : Stream' ℕ
b : Stream' α
⊢ Stream'.drop (∑ j ∈ Finset.range pn, (a, b).1.tail j + (a, b).1.head) (a, b).2 =
    Stream'.drop (∑ k ∈ Finset.range pn, a (k + 1) + a 0) b
no goals