case refl
α : Type u_1
β : Type ?u.551
γ : Type ?u.554
s : Multiset α
nodup✝¹ nodup✝ : Nodup s
⊢ { val := s, nodup := nodup✝¹ } = { val := s, nodup := nodup✝ }
α : Type u_1
β : Type ?u.551
γ : Type ?u.554
s : Multiset α
nodup✝¹ : Nodup s
t : Multiset α
nodup✝ : Nodup t
h : { val := s, nodup := nodup✝¹ }.val = { val := t, nodup := nodup✝ }.val
⊢ { val := s, nodup := nodup✝¹ } = { val := t, nodup := nodup✝ }
cases h
no goals
case refl
α : Type u_1
β : Type ?u.551
γ : Type ?u.554
s : Multiset α
nodup✝¹ nodup✝ : Nodup s
⊢ { val := s, nodup := nodup✝¹ } = { val := s, nodup := nodup✝ }
rfl