Cases on hidden argument

Stream: new members

[Andre Knispel]

I'm having a hypothesis that uses dite, and I'm trying to reduce it by using cases, but I've only managed to get proofs that the condition holds or doesn't hold, but I couldn't reduce dite so far. I assume if I had @dite h d x y, cases d would work, but I don't have d in context right now (at least not conveniently). How would I reduce dite?

[Kevin Buzzard]

dif_pos and dif_neg for refined control and split_ifs for a blunt instrument