no goals
α : Type u_1
p : α → Bool
x : α
xs l₂ : List α
h : ∀ (b : α), b ∈ x :: xs → ¬p b = true
⊢ eraseP p (x :: xs ++ l₂) = x :: xs ++ eraseP p l₂
simp [(forall_mem_cons.1 h).1, eraseP_append_right _ (forall_mem_cons.1 h).2]