cases hseq with
| seq _ _ _ u _ hS₂ hT₂ =>
  apply BigStep.seq
  { rw [BigStepEquiv] at hS
    rw [hS]
    assumption }
  { rw [BigStepEquiv] at hT
    rw [hT]
    assumption }
case mpr
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hseq : (S₂; T₂, s) ⟹ t
⊢ (S₁; T₁, s) ⟹ t
no goals