case a
α : Type u
β : Type v
γ : Type w
f : α → β
s : Stream' (Option α)
al : IsSeq s
⊢ ↑(map f (tail { val := s, property := al })) = ↑(tail (map f { val := s, property := al }))
α : Type u
β : Type v
γ : Type w
f : α → β
s : Stream' (Option α)
al : IsSeq s
⊢ map f (tail { val := s, property := al }) = tail (map f { val := s, property := al })
apply Subtype.eq
no goals
case a
α : Type u
β : Type v
γ : Type w
f : α → β
s : Stream' (Option α)
al : IsSeq s
⊢ ↑(map f (tail { val := s, property := al })) = ↑(tail (map f { val := s, property := al }))
dsimp [tail, map]