no goals
α : Type u_1
β : Type ?u.35311
γ : Type ?u.35314
s✝ t : Multiset α
a✝ : α
s : Multiset α
a : α
l : List α
this : l <+~ a :: l ∧ ¬l ~ a :: l
⊢ Quot.mk Setoid.r l < a ::ₘ Quot.mk Setoid.r l
simpa [lt_iff_le_and_ne]