case mk.mk
α : Type u_1
β : Type ?u.12536
γ : Type ?u.12539
a : α
s✝ : Multiset α
l₁ : List α
t✝ : Multiset α
l₂ : List α
⊢ a ::ₘ Quot.mk Setoid.r l₁ = a ::ₘ Quot.mk Setoid.r l₂ ↔ Quot.mk Setoid.r l₁ = Quot.mk Setoid.r l₂
α : Type u_1
β : Type ?u.12536
γ : Type ?u.12539
a : α
⊢ ∀ {s t : Multiset α}, a ::ₘ s = a ::ₘ t ↔ s = t
rintro ⟨l₁⟩ ⟨l₂⟩
no goals
case mk.mk
α : Type u_1
β : Type ?u.12536
γ : Type ?u.12539
a : α
s✝ : Multiset α
l₁ : List α
t✝ : Multiset α
l₂ : List α
⊢ a ::ₘ Quot.mk Setoid.r l₁ = a ::ₘ Quot.mk Setoid.r l₂ ↔ Quot.mk Setoid.r l₁ = Quot.mk Setoid.r l₂
simp