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