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

case mpr.while_false.hbody
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ (Stmt.skip, s) ⟹ s