no goals
ι : Type ?u.381634
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂✝ : List α
p : α → Bool
l₂ : List α
⊢ loop p [] l₂ = (reverse l₂ ++ takeWhile p [], dropWhile p [])
simp [span.loop, takeWhile, dropWhile]
no goals
ι : Type ?u.381634
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂✝ : List α
p : α → Bool
a : α
l l₂ : List α
⊢ loop p (a :: l) l₂ = (reverse l₂ ++ takeWhile p (a :: l), dropWhile p (a :: l))
cases hp : p a <;> simp [hp, span.loop, span.loop_eq_take_drop, takeWhile, dropWhile]