no goals
α : Sort u_1
p q r : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a✝ b✝ c✝ : α
a : p → q → α
b : p → ¬q → α
c : ¬p → α
⊢ dite p (fun hp => dite q (a hp) (b hp)) c =
    if hq : q then dite p (fun hp => a hp hq) c else dite p (fun hp => b hp hq) c
split_ifs <;> rfl