cases h with
| while_true _ _ _ t _ hB hS hw =>
  apply Or.intro_left
  apply Exists.intro t
  aesop
| while_false _ _ _ hB =>
  apply Or.intro_right
  aesop
case mp
B : State → Prop
S : Stmt
s u : State
h : (Stmt.whileDo B S, s) ⟹ u
⊢ (∃ t, B s ∧ (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u) ∨ ¬B s ∧ u = s
no goals