apply Or.intro_right
case mp.while_false
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ (∃ t, B s ∧ (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ s) ∨ ¬B s ∧ s = s
case mp.while_false.h
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ ¬B s ∧ s = s