{ intro hseq
  cases hseq
  apply Exists.intro
  apply And.intro <;>
    assumption }
case mp
S₁ S₂ : Stmt
s t : State
⊢ (S₁; S₂, s) ⟹ t → ∃ u, (S₁, s) ⟹ u ∧ (S₂, u) ⟹ t

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