α : Type u
β : Type v
γ : Type w
s : Seq α
⊢ Option.rec nil Prod.snd (Option.map (fun a => (a, ↑(Seq.tail s))) (Seq.head s)) = ↑(Seq.tail s)
α : Type u
β : Type v
γ : Type w
s : Seq α
⊢ tail ↑s = ↑(Seq.tail s)
simp [tail]
case h1
α : Type u
β : Type v
γ : Type w
⊢ nil = some <$> Seq.nil
α : Type u
β : Type v
γ : Type w
s : Seq α
⊢ Option.rec nil Prod.snd (Option.map (fun a => (a, ↑(Seq.tail s))) (Seq.head s)) = ↑(Seq.tail s)
induction' s using Seq.recOn with x s <;> simp [ofSeq]
no goals
case h1
α : Type u
β : Type v
γ : Type w
⊢ nil = some <$> Seq.nil
rfl