cases hskip
case mp.if_false
B : State → Prop
S : Stmt
s t : State
hB : ¬B s
hskip : (Stmt.skip, s) ⟹ t
⊢ (Stmt.whileDo B S, s) ⟹ t
case mp.if_false.skip
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ (Stmt.whileDo B S, s) ⟹ s