apply Iff.intro
S T : Stmt
s u : State
⊢ (S; T, s) ⟹ u ↔ ∃ t, (S, s) ⟹ t ∧ (T, t) ⟹ u
case mp
S T : Stmt
s u : State
⊢ (S; T, s) ⟹ u → ∃ t, (S, s) ⟹ t ∧ (T, t) ⟹ u

case mpr
S T : Stmt
s u : State
⊢ (∃ t, (S, s) ⟹ t ∧ (T, t) ⟹ u) → (S; T, s) ⟹ u