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