no goals
α : Type u
β : Type v
δ : Type w
a : α
⊢ [a] ≠ []
simp
no goals
α : Type u
β✝ : Type v
δ : Type w
a : α
β : Type u
fr : Stream' α → β
ch : fr (cycle [a] (_ : ¬[a] = [])) = fr (const a)
⊢ fr (tail (cycle [a] (_ : ¬[a] = []))) = fr (tail (const a))
rwa [cycle_eq, const_eq]