apply Or.intro_left
case mp.seq_step
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)) ∨ S = Stmt.skip ∧ (S'; T, s') = (T, 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)