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