case a
α : Type u
β : Type v
γ : Type w
a : α
s : Stream' α
⊢ ↑↑(a :: s) = ↑(cons a ↑s)
α : Type u
β : Type v
γ : Type w
a : α
s : Stream' α
⊢ ↑(a :: s) = cons a ↑s
apply Subtype.eq
case a
α : Type u
β : Type v
γ : Type w
a : α
s : Stream' α
⊢ Stream'.map some (a :: s) = some a :: Stream'.map some s
case a
α : Type u
β : Type v
γ : Type w
a : α
s : Stream' α
⊢ ↑↑(a :: s) = ↑(cons a ↑s)
simp [ofStream, cons]
no goals
case a
α : Type u
β : Type v
γ : Type w
a : α
s : Stream' α
⊢ Stream'.map some (a :: s) = some a :: Stream'.map some s
rw [Stream'.map_cons]