induction e₁ generalizing s₂ <;> cases e₂
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
out : Reaction.Output
e₁ : s -[out]→ s₁
e₂ : s -[out]→ s₂
⊢ s₁ = s₂
case refl.refl
α : Type
inst✝ : Readable α
s s₁ : State α
out : Reaction.Output
s✝ : State α
⊢ s✝ = s✝

case trans.trans
α : Type
inst✝ : Readable α
s s₁ : State α
out : Reaction.Output
hd✝ : Change
s₁✝ s₂✝¹ : State α
tl✝ : Reaction.Output
s₃✝ : State α
a✝³ : s₁✝ -[hd✝]→ s₂✝¹
a✝² : s₂✝¹ -[tl✝]→ s₃✝
a_ih✝ : ∀ {s₂ : State α}, s₂✝¹ -[tl✝]→ s₂ → s₃✝ = s₂
s₂ s₂✝ : State α
a✝¹ : s₁✝ -[hd✝]→ s₂✝
a✝ : s₂✝ -[tl✝]→ s₂
⊢ s₃✝ = s₂