rw [hus]
case mpr.inr.intro
B : State → Prop
S : Stmt
s u : State
hB : ¬B s
hus : u = s
⊢ (Stmt.whileDo B S, s) ⟹ u
case mpr.inr.intro
B : State → Prop
S : Stmt
s u : State
hB : ¬B s
hus : u = s
⊢ (Stmt.whileDo B S, s) ⟹ s