induction S with
| skip =>
  simp
  intros T t hstep
  cases hstep
| assign x a =>
  simp
  apply Exists.intro Stmt.skip
  apply Exists.intro (s[x ↦ a s])
  apply SmallStep.assign
| seq S T ihS ihT =>
  simp
  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
| ifThenElse B S T ihS ihT =>
  simp
  cases Classical.em (B s) with
  | inl h =>
    apply Exists.intro S
    apply Exists.intro s
    apply SmallStep.if_true
    assumption
  | inr h =>
    apply Exists.intro T
    apply Exists.intro s
    apply SmallStep.if_false
    assumption
| whileDo B S ih =>
  simp
  apply Exists.intro
    (Stmt.ifThenElse B (S; Stmt.whileDo B S)
       Stmt.skip)
  apply Exists.intro s
  apply SmallStep.whileDo
S : Stmt
s : State
⊢ (¬∃ T t, (S, s) ⇒ (T, t)) ↔ S = Stmt.skip
no goals