cases hloop with
| loop_base S s =>
  apply Or.inl
  rfl
| loop_step S s t u hS hl =>
  apply Or.inr
  apply Exists.intro t
  aesop
case mp
S : Stmt
s u : State
hloop : (Stmt.loop S, s) ⟹ u
⊢ s = u ∨ ∃ t, (S, s) ⟹ t ∧ (Stmt.loop S, t) ⟹ u
no goals