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