unfold MultisetLt
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : LT α
h : WellFounded MultisetRedLt
⊢ WellFounded MultisetLt
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : LT α
h : WellFounded MultisetRedLt
⊢ WellFounded (TC MultisetRedLt)