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