have s1 : x ∈ l1.diff l2 := List.mem_diff_of_mem h1 h2
α : Type
inst✝ : DecidableEq α
l1 l2 : List α
x : α
h1 : x ∈ l1
h2 : x ∉ l2
⊢ ((l1.diff l2).erase x).length < (l1.diff l2).length
α : Type
inst✝ : DecidableEq α
l1 l2 : List α
x : α
h1 : x ∈ l1
h2 : x ∉ l2
s1 : x ∈ l1.diff l2
⊢ ((l1.diff l2).erase x).length < (l1.diff l2).length