{ rw [BigStepEquiv] at hS
  rw [← hS]
  assumption }
case mp.seq.hS
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t u : State
hS₁ : (S₁, s) ⟹ u
hT₁ : (T₁, u) ⟹ t
⊢ (S₂, s) ⟹ ?mp.seq.t

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₂, ?mp.seq.t) ⟹ t

case mp.seq.t
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t u : State
hS₁ : (S₁, s) ⟹ u
hT₁ : (T₁, u) ⟹ t
⊢ State
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