induction e₁ generalizing s₂ <;> cases e₂
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
ht : s₁.tag = s₂.tag
e₁ : RTC s s₁
e₂ : RTC s s₂
⊢ s₁ = s₂
case refl.refl
α : Type
inst✝ : Proper α
s s₁ s✝ : State α
ht : s✝.tag = s✝.tag
⊢ s✝ = s✝

case refl.trans
α : Type
inst✝ : Proper α
s s₁ s✝ s₂ : State α
ht : s✝.tag = s₂.tag
s₂✝ : State α
a✝¹ : s✝ ↓ₜ s₂✝
a✝ : RTC s₂✝ s₂
⊢ s✝ = s₂

case trans.refl
α : Type
inst✝ : Proper α
s s₁ s₁✝ s₂✝ s₃✝ : State α
a✝¹ : s₁✝ ↓ₜ s₂✝
a✝ : RTC s₂✝ s₃✝
a_ih✝ : ∀ {s₂ : State α}, s₃✝.tag = s₂.tag → RTC s₂✝ s₂ → s₃✝ = s₂
ht : s₃✝.tag = s₁✝.tag
⊢ s₃✝ = s₁✝

case trans.trans
α : Type
inst✝ : Proper α
s s₁ s₁✝ s₂✝¹ s₃✝ : State α
a✝³ : s₁✝ ↓ₜ s₂✝¹
a✝² : RTC s₂✝¹ s₃✝
a_ih✝ : ∀ {s₂ : State α}, s₃✝.tag = s₂.tag → RTC s₂✝¹ s₂ → s₃✝ = s₂
s₂ : State α
ht : s₃✝.tag = s₂.tag
s₂✝ : State α
a✝¹ : s₁✝ ↓ₜ s₂✝
a✝ : RTC s₂✝ s₂
⊢ s₃✝ = s₂