{ intro hif
  cases hif with
  | if_true _ _ _ _ _ hB hseq =>
    cases hseq with
    | seq _ _ _ u _ hS hT =>
      apply BigStep.while_true <;>
        assumption
  | if_false _ _ _ _ _ hB hskip =>
    cases hskip
    apply BigStep.while_false
    assumption }
case mp
B : State → Prop
S : Stmt
s t : State
⊢ (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) ⟹ t → (Stmt.whileDo B S, s) ⟹ t

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
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