cases hex with
| intro S' hex' =>
  cases hex' with
  | intro s' hand =>
    cases hand with
    | intro hS hUt =>
      rw [hUt]
      apply SmallStep.seq_step
      assumption
case mpr.inl
S T : Stmt
s : State
Ut : Stmt × State
hex : ∃ S' t, (S, s) ⇒ (S', t) ∧ Ut = (S'; T, t)
⊢ (S; T, s) ⇒ Ut
no goals