rw [hUt]
case mpr.inl.intro.intro.intro
S T : Stmt
s : State
Ut : Stmt × State
S' : Stmt
s' : State
hS : (S, s) ⇒ (S', s')
hUt : Ut = (S'; T, s')
⊢ (S; T, s) ⇒ Ut
case mpr.inl.intro.intro.intro
S T : Stmt
s : State
Ut : Stmt × State
S' : Stmt
s' : State
hS : (S, s) ⇒ (S', s')
hUt : Ut = (S'; T, s')
⊢ (S; T, s) ⇒ (S'; T, s')