cases e₁ <;> cases e₂ <;> simp [rcn] at h
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
e₁ : s ↓ᵢ s₁
e₂ : s ↓ᵢ s₂
h : rcn e₁ = rcn e₂
⊢ s₁ = s₂
case skip.skip
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
s✝¹ : s ↓ₛ s₁
s✝ : s ↓ₛ s₂
h : Step.Skip.rcn s✝¹ = Step.Skip.rcn s✝
⊢ s₁ = s₂

case skip.exec
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
s✝ : s ↓ₛ s₁
e✝ : s ↓ₑ s₂
h : Step.Skip.rcn s✝ = Step.Exec.rcn e✝
⊢ s₁ = s₂

case exec.skip
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
e✝ : s ↓ₑ s₁
s✝ : s ↓ₛ s₂
h : Step.Exec.rcn e✝ = Step.Skip.rcn s✝
⊢ s₁ = s₂

case exec.exec
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
e✝¹ : s ↓ₑ s₁
e✝ : s ↓ₑ s₂
h : Step.Exec.rcn e✝¹ = Step.Exec.rcn e✝
⊢ s₁ = s₂