case cons
ι : Type ?u.292233
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (acc : List α), go p tail✝ acc ≠ []
acc : List α
⊢ ¬(if p head✝ = true then reverse acc :: go p tail✝ [] else go p tail✝ (head✝ :: acc)) = []
ι : Type ?u.292233
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs✝ ys : List α
ls : List (List α)
f : List α → List α
xs acc : List α
⊢ go p xs acc ≠ []
induction xs generalizing acc <;> simp [go]
no goals
case cons
ι : Type ?u.292233
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (acc : List α), go p tail✝ acc ≠ []
acc : List α
⊢ ¬(if p head✝ = true then reverse acc :: go p tail✝ [] else go p tail✝ (head✝ :: acc)) = []
split <;> simp [*]