α : Type u
β : Type v
δ : Type w
f : α → β → δ
s₁ : Stream' α
s₂ : Stream' β
⊢ head (zip f s₁ s₂) :: tail (zip f s₁ s₂) = f (head s₁) (head s₂) :: zip f (tail s₁) (tail s₂)
α : Type u
β : Type v
δ : Type w
f : α → β → δ
s₁ : Stream' α
s₂ : Stream' β
⊢ zip f s₁ s₂ = f (head s₁) (head s₂) :: zip f (tail s₁) (tail s₂)
rw [← Stream'.eta (zip f s₁ s₂)]
no goals
α : Type u
β : Type v
δ : Type w
f : α → β → δ
s₁ : Stream' α
s₂ : Stream' β
⊢ head (zip f s₁ s₂) :: tail (zip f s₁ s₂) = f (head s₁) (head s₂) :: zip f (tail s₁) (tail s₂)
rfl