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
hor : (∃ S' t, (S, s) ⇒ (S', t) ∧ Ut = (S'; T, t)) ∨ S = Stmt.skip ∧ Ut = (T, s)
⊢ (S; T, s) ⇒ Ut
no goals