assumption
case mpr.seq.hS
S₁ S₂ T₁ T₂ : Stmt
hS✝ : S₁ ~ S₂
hS : ∀ (s t : State), (S₁, s) ⟹ t ↔ (S₂, s) ⟹ t
hT : T₁ ~ T₂
s t u : State
hS₂ : (S₂, s) ⟹ u
hT₂ : (T₂, u) ⟹ t
⊢ (S₂, s) ⟹ ?m.68939 hT s t u hS₂ hT₂

S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
⊢ T₁ ~ T₂ → (s t u : State) → (S₂, s) ⟹ u → (T₂, u) ⟹ t → State
no goals