{ intro h
  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
⊢ (Stmt.whileDo B S, s) ⟹ u → (∃ t, B s ∧ (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u) ∨ ¬B s ∧ u = s

case mpr
B : State → Prop
S : Stmt
s u : State
⊢ (∃ t, B s ∧ (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u) ∨ ¬B s ∧ u = s → (Stmt.whileDo B S, s) ⟹ u
case mpr
B : State → Prop
S : Stmt
s u : State
⊢ (∃ t, B s ∧ (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u) ∨ ¬B s ∧ u = s → (Stmt.whileDo B S, s) ⟹ u