{ intro hor
  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
⊢ (s = u ∨ ∃ t, (S, s) ⟹ t ∧ (Stmt.loop S, t) ⟹ u) → (Stmt.loop S, s) ⟹ u
no goals