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

case mpr
Ss : List Stmt
s t : State
⊢ (∃ i hless, (Ss[i], s) ⟹ t) → (Stmt.choice Ss, s) ⟹ t
case mpr
Ss : List Stmt
s t : State
⊢ (∃ i hless, (Ss[i], s) ⟹ t) → (Stmt.choice Ss, s) ⟹ t