Is there a tactic for unfolding all Definitions (in the goal, optionally also in hypotheses)? Something shorter than unfold def, def0, ... in *.
You can use cbv delta in * for example.
See https://coq.inria.fr/distrib/current/refman/proof-engine/tactics.html?highlight=cbv#coq:tacn.cbv