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