case mk
α : Type u_1
β : Type ?u.12839
γ : Type ?u.12842
p : Multiset α → Prop
empty : p 0
cons : ∀ ⦃a : α⦄ {s : Multiset α}, p s → p (a ::ₘ s)
s✝ : Multiset α
l : List α
⊢ p (Quot.mk Setoid.r l)
α : Type u_1
β : Type ?u.12839
γ : Type ?u.12842
p : Multiset α → Prop
empty : p 0
cons : ∀ ⦃a : α⦄ {s : Multiset α}, p s → p (a ::ₘ s)
⊢ ∀ (s : Multiset α), p s
rintro ⟨l⟩
no goals
case mk
α : Type u_1
β : Type ?u.12839
γ : Type ?u.12842
p : Multiset α → Prop
empty : p 0
cons : ∀ ⦃a : α⦄ {s : Multiset α}, p s → p (a ::ₘ s)
s✝ : Multiset α
l : List α
⊢ p (Quot.mk Setoid.r l)
induction' l with _ _ ih <;> [exact empty; exact cons ih]