{ intro hwhile
  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
⊢ (Stmt.whileDo B S, s) ⟹ t → (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) ⟹ t
no goals