{ intro hST
  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
⊢ (S; T, s) ⇒ Ut → (∃ S' t, (S, s) ⇒ (S', t) ∧ Ut = (S'; T, t)) ∨ S = Stmt.skip ∧ Ut = (T, s)

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
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