apply Iff.intro
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 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