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