{ rw [BigStepEquiv] at hS
  rw [hS]
  assumption }
case mpr.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) ⟹ ?mpr.seq.t

case mpr.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₁, ?mpr.seq.t) ⟹ t

case mpr.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 mpr.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