apply Iff.intro
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
⊢ (Stmt.ifThenElse B S₁ T₁, s) ⟹ t ↔ (Stmt.ifThenElse B S₂ T₂, s) ⟹ t
case mp
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
⊢ (Stmt.ifThenElse B S₁ T₁, s) ⟹ t → (Stmt.ifThenElse B S₂ T₂, s) ⟹ t

case mpr
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
⊢ (Stmt.ifThenElse B S₂ T₂, s) ⟹ t → (Stmt.ifThenElse B S₁ T₁, s) ⟹ t