case a
α : Type u
β : Type v
δ : Type w
a : α
⊢ ∀ (n : ℕ), nth (const a) n = nth (a :: const a) n
α : Type u
β : Type v
δ : Type w
a : α
⊢ const a = a :: const a
apply Stream'.ext
case a
α : Type u
β : Type v
δ : Type w
a : α
n : ℕ
⊢ nth (const a) n = nth (a :: const a) n
case a
α : Type u
β : Type v
δ : Type w
a : α
⊢ ∀ (n : ℕ), nth (const a) n = nth (a :: const a) n
intro n
no goals
case a
α : Type u
β : Type v
δ : Type w
a : α
n : ℕ
⊢ nth (const a) n = nth (a :: const a) n
cases n <;> rfl