cases hST with
| seq_step _ S' _ _ s' hS =>
  apply Or.intro_left
  apply Exists.intro S'
  apply Exists.intro s'
  aesop
| seq_skip =>
  apply Or.intro_right
  aesop
case mp
S T : Stmt
s : State
Ut : Stmt × State
hST : (S; T, s) ⇒ Ut
⊢ (∃ S' t, (S, s) ⇒ (S', t) ∧ Ut = (S'; T, t)) ∨ S = Stmt.skip ∧ Ut = (T, s)
no goals