apply BigStep.while_true <;>
  assumption
case mpr.inl.intro.intro.intro
B : State → Prop
S : Stmt
s u t : State
hB : B s
hS : (S, s) ⟹ t
hwhile : (Stmt.whileDo B S, t) ⟹ u
⊢ (Stmt.whileDo B S, s) ⟹ u
no goals