rw [BigStepEquiv] at hT
case mp.seq.hT
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t u : State
hS₁ : (S₁, s) ⟹ u
hT₁ : (T₁, u) ⟹ t
⊢ (T₂, u) ⟹ t
case mp.seq.hT
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : ∀ (s t : State), (T₁, s) ⟹ t ↔ (T₂, s) ⟹ t
s t u : State
hS₁ : (S₁, s) ⟹ u
hT₁ : (T₁, u) ⟹ t
⊢ (T₂, u) ⟹ t