Unify case_bool_decide / case_decide
We have case_bool_decide
and 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.