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