cases hand with
| intro hB hUs =>
  rw [hUs]
  apply SmallStep.if_false
  assumption
case mpr.inr
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
hand : ¬B s ∧ Us = (T, s)
⊢ (Stmt.ifThenElse B S T, s) ⇒ Us
no goals