cases hseq with
| seq _ _ _ u _ hS hT =>
  apply BigStep.while_true <;>
    assumption
case mp.if_true
B : State → Prop
S : Stmt
s t : State
hB : B s
hseq : (S; Stmt.whileDo B S, s) ⟹ t
⊢ (Stmt.whileDo B S, s) ⟹ t
no goals