Есть ли тактика для разворачивания всех Definition с (в цели, по желанию также в гипотезах)? Что-то короче unfold def, def0, ... in *.
Definition
unfold def, def0, ... in *.
Вы можете использовать cbv delta in * например.
cbv delta in *
См. https://coq.inria.fr/distrib/current/refman/proof-engine/tactics.html?highlight=cbv#coq:tacn.cbv