induction e' generalizing s₁ <;> simp [rcns] at *
α : Type
inst✝ : Proper α
s s₁ s₂ s₃ : State α
i : ID
e : s₁ ↓ᵢ s₂
e' : s₂ ↓ᵢ+ s₃
hm : i ∈ rcns e'
hr : rcn e :: rcns e' ≮[s₁.rtr] i
⊢ ∃ f, rcns f = i :: rcn e :: List.erase (rcns e') i
case single
α : Type
inst✝ : Proper α
s s₂ s₃ : State α
i : ID
s₁✝ s₂✝ : State α
a✝ : s₁✝ ↓ᵢ s₂✝
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : [rcn e, rcn a✝] ≮[s₁.rtr] i
hm : i = rcn a✝
⊢ ∃ f, rcns f = i :: rcn e :: List.erase [rcn a✝] i

case trans
α : Type
inst✝ : Proper α
s s₂ s₃ : State α
i : ID
s₁✝ s₂✝ s₃✝ : State α
a✝¹ : s₁✝ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₃✝
a_ih✝ :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂✝),
    i ∈ rcns a✝ → (rcn e :: rcns a✝ ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns a✝) i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : rcn e :: rcn a✝¹ :: rcns a✝ ≮[s₁.rtr] i
hm : i = rcn a✝¹ ∨ i ∈ rcns a✝
⊢ ∃ f, rcns f = i :: rcn e :: List.erase (rcn a✝¹ :: rcns a✝) i