refactor: deriving DecidableEq to use `termination_by structural`

[nomeata]

now that we support structural mutual recursion, I expect that every DecidableEq instance be implemented using structural recursion, so let's be explicit about it.