cases Classical.em (S = Stmt.skip) with
| inl h =>
  rw [h]
  apply Exists.intro T
  apply Exists.intro s
  apply SmallStep.seq_skip
| inr h =>
  simp [h] at ihS
  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
s : State
S T : Stmt
ihS : (¬∃ T t, (S, s) ⇒ (T, t)) ↔ S = Stmt.skip
ihT : (¬∃ T_1 t, (T, s) ⇒ (T_1, t)) ↔ T = Stmt.skip
⊢ ∃ T_1 t, (S; T, s) ⇒ (T_1, t)
no goals