α : Type u_1
β : Type ?u.25432
γ : Type ?u.25435
a b : α
⊢ a ::ₘ 0 = b ::ₘ 0 ↔ a = b
α : Type u_1
β : Type ?u.25432
γ : Type ?u.25435
a b : α
⊢ {a} = {b} ↔ a = b
simp_rw [← cons_zero]
no goals
α : Type u_1
β : Type ?u.25432
γ : Type ?u.25435
a b : α
⊢ a ::ₘ 0 = b ::ₘ 0 ↔ a = b
exact cons_inj_left _