The definition of default_dec_tac in core is broken, because unfold_sizeof could actually discharge the goal.

Here we add a test using done to detect this.

The default well_founded_tactics provided in core are broken in some situations, often indicated by the message

The nested exception contains the failure state for the decreasing tactic.
nested exception message:
tactic failed, there are no goals to be solved
state:
no goals

Use this replacement by adding

using_well_founded wf_tacs

at the end of your inductive definition.