cases hex with
| intro t hand =>
  cases hand with
  | intro hS hl =>
    apply BigStep.loop_step <;>
      assumption
case mpr.inr
S : Stmt
s u : State
hex : ∃ t, (S, s) ⟹ t ∧ (Stmt.loop S, t) ⟹ u
⊢ (Stmt.loop S, s) ⟹ u
no goals