intro a b
case h.e_a.zero
α : Type
⊢ ∀ (lengths : Stream' ℕ) (a : Stream' α),
    ((Stream'.iterate (fun x => (x.1.tail, Stream'.drop x.1.head x.2)) (lengths, a)).get 0).1.head = lengths 0
case h.e_a.zero
α : Type
a : Stream' ℕ
b : Stream' α
⊢ ((Stream'.iterate (fun x => (x.1.tail, Stream'.drop x.1.head x.2)) (a, b)).get 0).1.head = a 0