apply Exists.intro S'
case mp.seq_step.h
S T : Stmt
s : State
S' : Stmt
s' : State
hS : (S, s) ⇒ (S', s')
⊢ ∃ S'_1 t, (S, s) ⇒ (S'_1, t) ∧ (S'; T, s') = (S'_1; T, t)
case mp.seq_step.h
S T : Stmt
s : State
S' : Stmt
s' : State
hS : (S, s) ⇒ (S', s')
⊢ ∃ t, (S, s) ⇒ (S', t) ∧ (S'; T, s') = (S'; T, t)