cases h
α : Sort u_1
c : Prop
h : Decidable c
x y : α
⊢ if c then (if c then x else y) = x else (if c then x else y) = y
case isFalse
α : Sort u_1
c : Prop
x y : α
h✝ : ¬c
⊢ if c then (if c then x else y) = x else (if c then x else y) = y

case isTrue
α : Sort u_1
c : Prop
x y : α
h✝ : c
⊢ if c then (if c then x else y) = x else (if c then x else y) = y