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