cases hwhile with
| while_true _ _ _ u _ hB hS hw =>
  apply BigStep.if_true
  exact hB
  apply BigStep.seq <;>
    assumption
| while_false _ _ _ hB =>
  apply BigStep.if_false
  exact hB
  apply BigStep.skip
case mpr
B : State → Prop
S : Stmt
s t : State
hwhile : (Stmt.whileDo B S, s) ⟹ t
⊢ (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) ⟹ t
no goals