no goals
α : Type u
β : Type v
δ : Type w
x y : α
s t : Stream' α
h : x :: s = y :: t
⊢ x = y
rw [← nth_zero_cons x s, h, nth_zero_cons]
no goals
α : Type u
β : Type v
δ : Type w
x y : α
s t : Stream' α
h : x :: s = y :: t
n : ℕ
⊢ nth s n = nth t n
rw [← nth_succ_cons n _ x, h, nth_succ_cons]