rw [← hS]
case mp.if_true.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : ∀ (s t : State), (S₁, s) ⟹ t ↔ (S₂, s) ⟹ t
hT : T₁ ~ T₂
s t : State
hB : B s
hS₁ : (S₁, s) ⟹ t
⊢ (S₂, s) ⟹ t
case mp.if_true.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : ∀ (s t : State), (S₁, s) ⟹ t ↔ (S₂, s) ⟹ t
hT : T₁ ~ T₂
s t : State
hB : B s
hS₁ : (S₁, s) ⟹ t
⊢ (S₁, s) ⟹ t