no goals
α : Type u
β : Type v
δ : Type w
s : Stream' α
k n : ℕ
h : k + 1 < n + 1
⊢ List.get? (take (n + 1) s) (k + 1) = some (nth s (k + 1))
rw [take_succ, List.get?, get?_take (Nat.lt_of_succ_lt_succ h), nth_succ]