{ intro h
  cases h with
  | intro s' h' =>
    cases h' with
    | intro hS hT =>
      apply BigStep.seq <;>
        assumption }
case mpr
S T : Stmt
s u : State
⊢ (∃ t, (S, s) ⟹ t ∧ (T, t) ⟹ u) → (S; T, s) ⟹ u
no goals