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