induction e <;> try cases ‹_ ↓ _›
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
triv : State.Trivial s₁
e : s₁ ⇓ s₂
⊢ Step.Time.RTC s₁ s₂
case refl
α : Type
inst✝ : Proper α
s s₁ s₂ s✝ : State α
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₃✝