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