α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
h : ¬a ∈ l
⊢ length (a :: l) = length l + 1
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
h : ¬a ∈ l
⊢ length (List.insert a l) = length l + 1
rw [insert_of_not_mem h]
no goals
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
h : ¬a ∈ l
⊢ length (a :: l) = length l + 1
rfl