α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
⊢ tail s₁ ⋈ tail s₂ = tail (tail (head s₁ :: head s₂ :: (tail s₁ ⋈ tail s₂)))
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
⊢ tail s₁ ⋈ tail s₂ = tail (tail (s₁ ⋈ s₂))
rw [interleave_eq s₁ s₂]
no goals
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
⊢ tail s₁ ⋈ tail s₂ = tail (tail (head s₁ :: head s₂ :: (tail s₁ ⋈ tail s₂)))
rfl