simp only [h₁, h₂, h₃]
c₁ c₂ : Prop
α : Sort u_1
inst✝¹ : Decidable c₁
inst✝ : Decidable c₂
t₁ t₂ e₁ e₂ : α
h₁ : c₁ = c₂
h₂ : t₁ = t₂
h₃ : e₁ = e₂
⊢ (if c₁ then t₁ else e₁) = if c₂ then t₂ else e₂
no goals