cases hex with
| intro i hex =>
  cases hex with
  | intro hless hstep =>
  apply BigStep.choice <;>
    assumption
case mpr
Ss : List Stmt
s t : State
hex : ∃ i hless, (Ss[i], s) ⟹ t
⊢ (Stmt.choice Ss, s) ⟹ t
no goals