Theorem: equiv_r_wf (Pdl/MultisetOrder.lean)

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

State before:
α : Type u_1
r1 : Multiset α → Multiset α → Prop
inst✝¹ : DecidableEq α
inst✝ : LT α
h1 : WellFounded r1
⊢ WellFounded r1
Tactic:
simp_all only
State after:
no goals