α : Type u
β : Type v
δ : Type w
s : Stream' α
⊢ corec id tail (tail s) = tail s :: corec id tail (tail (tail s))
α : Type u
β : Type v
δ : Type w
s : Stream' α
⊢ tails s = tail s :: tails (tail s)
unfold tails
α : Type u
β : Type v
δ : Type w
s : Stream' α
⊢ id (tail s) :: corec id tail (tail (tail s)) = tail s :: corec id tail (tail (tail s))
α : Type u
β : Type v
δ : Type w
s : Stream' α
⊢ corec id tail (tail s) = tail s :: corec id tail (tail (tail s))
rw [corec_eq]
no goals
α : Type u
β : Type v
δ : Type w
s : Stream' α
⊢ id (tail s) :: corec id tail (tail (tail s)) = tail s :: corec id tail (tail (tail s))
rfl