cases ‹_ ↓ _›
case trans
α : Type
inst✝ : Proper α
s s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝¹ : s₁✝ ↓ s₂✝
a✝ : s₂✝ ⇓ s₃✝
a_ih✝ : State.Trivial s₂✝ → Step.Time.RTC s₂✝ s₃✝
triv : State.Trivial s₁✝
⊢ Step.Time.RTC s₁✝ s₃✝
case trans.skip
α : Type
inst✝ : Proper α
s s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝ : s₂✝ ⇓ s₃✝
a_ih✝ : State.Trivial s₂✝ → Step.Time.RTC s₂✝ s₃✝
triv : State.Trivial s₁✝
s✝ : s₁✝ ↓ₛ s₂✝
⊢ Step.Time.RTC s₁✝ s₃✝

case trans.exec
α : Type
inst✝ : Proper α
s s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝ : s₂✝ ⇓ s₃✝
a_ih✝ : State.Trivial s₂✝ → Step.Time.RTC s₂✝ s₃✝
triv : State.Trivial s₁✝
e✝ : s₁✝ ↓ₑ s₂✝
⊢ Step.Time.RTC s₁✝ s₃✝

case trans.time
α : Type
inst✝ : Proper α
s s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝ : s₂✝ ⇓ s₃✝
a_ih✝ : State.Trivial s₂✝ → Step.Time.RTC s₂✝ s₃✝
triv : State.Trivial s₁✝
t✝ : s₁✝ ↓ₜ s₂✝
⊢ Step.Time.RTC s₁✝ s₃✝