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