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