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