case exec.exec e₁ e₂ => simp [e₁.dst_eq, e₂.dst_eq, h, e₁.apply.deterministic (h.symm ▸ e₂.apply)]
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
e₁ : s ↓ₑ s₁
e₂ : s ↓ₑ s₂
h : Step.Exec.rcn e₁ = Step.Exec.rcn e₂
⊢ s₁ = s₂
no goals