induction s using Quotient.inductionOn with | _ L =>
exact hmotive rfl
α : Type u_1
β : Type u_2
s : Multiset α
f : (L : List α) → ↑L = s → β
h : ∀ (a b : List α) (ha : ↑a = s) (hb : ↑b = s), f a ha = f b hb
motive : Prop
hmotive : ∀ {L : List α} {hL : ↑L = s}, elim s f h = f L hL → motive
⊢ motive
no goals