Theorem: Lt_wf (Pdl/MultisetOrder.lean)

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

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : LT α
h : WellFounded MultisetRedLt
⊢ WellFounded (TC MultisetRedLt)
Tactic:
apply TC.wf
State after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : LT α
h : WellFounded MultisetRedLt
⊢ WellFounded MultisetRedLt

State before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : LT α
h : WellFounded MultisetRedLt
⊢ WellFounded MultisetRedLt
Tactic:
assumption
State after:
no goals