match Classical.em c with
| Or.inl hc  => rw [if_pos hc, if_pos hc]
| Or.inr hnc => rw [if_neg hnc, if_neg hnc]
α : Type u
c : Prop
t e : α
⊢ if c then (if c then t else e) = t else (if c then t else e) = e
no goals