cases hseq
case mp
S₁ S₂ : Stmt
s t : State
hseq : (S₁; S₂, s) ⟹ t
⊢ ∃ u, (S₁, s) ⟹ u ∧ (S₂, u) ⟹ t
case mp.seq
S₁ S₂ : Stmt
s t t✝ : State
hS✝ : (S₁, s) ⟹ t✝
hT✝ : (S₂, t✝) ⟹ t
⊢ ∃ u, (S₁, s) ⟹ u ∧ (S₂, u) ⟹ t