cases hchoice with
| choice _ _ _ i hless hbody =>
  apply Exists.intro i
  apply Exists.intro hless
  assumption
case mp
Ss : List Stmt
s t : State
hchoice : (Stmt.choice Ss, s) ⟹ t
⊢ ∃ i hless, (Ss[i], s) ⟹ t
no goals