intro hseq
case mpr
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
⊢ (S₂; T₂, s) ⟹ t → (S₁; T₁, s) ⟹ t
case mpr
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hseq : (S₂; T₂, s) ⟹ t
⊢ (S₁; T₁, s) ⟹ t