apply SmallStep.if_false
case while_false.hbc
Ss : Stmt × State
t : State
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) ⇒ (Stmt.skip, s)
case while_false.hbc.hcond
Ss : Stmt × State
t : State
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ ¬B s