apply BigStep.while_false
case mp.if_false.skip
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ (Stmt.whileDo B S, s) ⟹ s
case mp.if_false.skip.hcond
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ ¬B s