Unify case_bool_decide / case_decide
case_decide, but things still get annoying when the goal contains both a
decide and a
bool_decide for the same proposition: you have to either destruct twice or manually
rewrite /bool_decide_decie. See e.g. here.
Maybe the two tactics should be unified by just making
case_decide start with
rewrite /bool_decide_decie or so.