cases e₁ <;> cases e₂
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ᵢ s₂
e₂ : s₂ ↓ᵢ s₃
h : rcn e₁ ≮[s₁.rtr]≯ rcn e₂
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn e₂ ∧ rcn e₂' = rcn e₁ ∧ s₃' = s₃
case skip.skip
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
s✝¹ : s₁ ↓ₛ s₂
s✝ : s₂ ↓ₛ s₃
h : rcn (skip s✝¹) ≮[s₁.rtr]≯ rcn (skip s✝)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip s✝) ∧ rcn e₂' = rcn (skip s✝¹) ∧ s₃' = s₃

case skip.exec
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
s✝ : s₁ ↓ₛ s₂
e✝ : s₂ ↓ₑ s₃
h : rcn (skip s✝) ≮[s₁.rtr]≯ rcn (exec e✝)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e✝) ∧ rcn e₂' = rcn (skip s✝) ∧ s₃' = s₃

case exec.skip
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e✝ : s₁ ↓ₑ s₂
s✝ : s₂ ↓ₛ s₃
h : rcn (exec e✝) ≮[s₁.rtr]≯ rcn (skip s✝)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip s✝) ∧ rcn e₂' = rcn (exec e✝) ∧ s₃' = s₃

case exec.exec
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e✝¹ : s₁ ↓ₑ s₂
e✝ : s₂ ↓ₑ s₃
h : rcn (exec e✝¹) ≮[s₁.rtr]≯ rcn (exec e✝)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e✝) ∧ rcn e₂' = rcn (exec e✝¹) ∧ s₃' = s₃