revert d l r
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
d l r : Bool
⊢ (if d = true then l else r) = (d && l || !d && r)
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
⊢ ∀ (d l r : Bool), (if d = true then l else r) = (d && l || !d && r)