case trans.inl e e' h =>
  exists trans e e'
  simp [rcns, h]
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
s₂✝ : State α
e : s₁ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₂
hr : rcn e :: rcns e' ≮[s₁.rtr] i
h : i = rcn e
⊢ ∃ e'_1, rcns e'_1 = i :: List.erase (rcn e :: rcns e') i
no goals