{ intro h
  cases h with
  | seq =>
    apply Exists.intro
    apply And.intro <;>
      assumption }
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
case mpr
S T : Stmt
s u : State
⊢ (∃ t, (S, s) ⟹ t ∧ (T, t) ⟹ u) → (S; T, s) ⟹ u