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