subst h2
α : Type u_1
r1 r2 : Multiset α → Multiset α → Prop
inst✝¹ : DecidableEq α
inst✝ : LT α
h1 : WellFounded r1
h2 : r1 = r2
⊢ WellFounded r2
α : Type u_1
r1 : Multiset α → Multiset α → Prop
inst✝¹ : DecidableEq α
inst✝ : LT α
h1 : WellFounded r1
⊢ WellFounded r1