rw [hUs]
case mpr.inl.intro
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
hB : B s
hUs : Us = (S, s)
⊢ (Stmt.ifThenElse B S T, s) ⇒ Us
case mpr.inl.intro
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
hB : B s
hUs : Us = (S, s)
⊢ (Stmt.ifThenElse B S T, s) ⇒ (S, s)