Theorem: List.eq_remove_cons (Logic/Vorspiel/Vorspiel.lean)

State before:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.173910 → Type ?u.173912
α : Type u_1
β : Type ?u.173918
inst✝¹ : Monad m
inst✝ : DecidableEq α
q : α
l : List α
⊢ remove q (q :: l) = remove q l
Tactic:
induction l <;> simp_all [List.remove]
State after:
no goals