{
  intro hor
  cases hor with
  | inl hex =>
    cases hex with
    | intro S' hex' =>
      cases hex' with
      | intro s' hand =>
        cases hand with
        | intro hS hUt =>
          rw [hUt]
          apply SmallStep.seq_step
          assumption
  | inr hand =>
    cases hand with
    | intro hS hUt =>
      rw [hS, hUt]
      apply SmallStep.seq_skip }
case mpr
S T : Stmt
s : State
Ut : Stmt × State
⊢ (∃ S' t, (S, s) ⇒ (S', t) ∧ Ut = (S'; T, t)) ∨ S = Stmt.skip ∧ Ut = (T, s) → (S; T, s) ⇒ Ut
no goals