cases ‹_ ∨ _›
case trans
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
s₂✝ : State α
a✝¹ : s₁ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₂
hr : rcn a✝¹ :: rcns a✝ ≮[s₁.rtr] i
hm : i = rcn a✝¹ ∨ i ∈ rcns a✝
⊢ ∃ e', rcns e' = i :: List.erase (rcn a✝¹ :: rcns a✝) i
case trans.inl
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
s₂✝ : State α
a✝¹ : s₁ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₂
hr : rcn a✝¹ :: rcns a✝ ≮[s₁.rtr] i
h✝ : i = rcn a✝¹
⊢ ∃ e', rcns e' = i :: List.erase (rcn a✝¹ :: rcns a✝) i

case trans.inr
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
s₂✝ : State α
a✝¹ : s₁ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₂
hr : rcn a✝¹ :: rcns a✝ ≮[s₁.rtr] i
h✝ : i ∈ rcns a✝
⊢ ∃ e', rcns e' = i :: List.erase (rcn a✝¹ :: rcns a✝) i