rcases s with ⟨s,h⟩
α : Type u_1
β : Type u_2
s : Finset α
f : (L : List α) → ↑L = s.val → β
h : ∀ (a b : List α) (ha : ↑a = s.val) (hb : ↑b = s.val), f a ha = f b hb
motive : Prop
hmotive : ∀ {L : List α} {hL : ↑L = s.val}, elim s f h = f L hL → motive
⊢ motive
case mk
α : Type u_1
β : Type u_2
motive : Prop
s : Multiset α
h✝ : Multiset.Nodup s
f : (L : List α) → ↑L = { val := s, nodup := h✝ }.val → β
h :
  ∀ (a b : List α) (ha : ↑a = { val := s, nodup := h✝ }.val) (hb : ↑b = { val := s, nodup := h✝ }.val), f a ha = f b hb
hmotive : ∀ {L : List α} {hL : ↑L = { val := s, nodup := h✝ }.val}, elim { val := s, nodup := h✝ } f h = f L hL → motive
⊢ motive