{ intro hseq
  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
⊢ (S₂; T₂, s) ⟹ t → (S₁; T₁, s) ⟹ t
no goals