α : Type u
β : Type v
γ : Type w
s : Seq α
⊢ get? s 0 = Prod.fst <$> (fun a' => (a', tail s)) <$> get? s 0
α : Type u
β : Type v
γ : Type w
s : Seq α
⊢ head s = Prod.fst <$> destruct s
unfold destruct head
no goals
α : Type u
β : Type v
γ : Type w
s : Seq α
⊢ get? s 0 = Prod.fst <$> (fun a' => (a', tail s)) <$> get? s 0
cases get? s 0 <;> rfl