cases hr with
| while_true _ _ _ s' _ hB' hS hw => aesop
| while_false _ _ _ hB'           => rfl
case while_false
Ss : Stmt × State
l : State
B : State → Prop
S : Stmt
s : State
hB : ¬B s
r : State
hr : (Stmt.whileDo B S, s) ⟹ r
⊢ s = r
no goals