cases hS₀ with
| intro s' hS =>
  apply Exists.intro (S'; T)
  apply Exists.intro s'
  apply SmallStep.seq_step
  assumption
case seq.inr.intro
s : State
S T : Stmt
ihT : (¬∃ T_1 t, (T, s) ⇒ (T_1, t)) ↔ T = Stmt.skip
h : ¬S = Stmt.skip
S' : Stmt
hS₀ : ∃ t, (S, s) ⇒ (S', t)
⊢ ∃ T_1 t, (S; T, s) ⇒ (T_1, t)
no goals