A quick find theories/ -name '*.v' -exec grep -Hn 'Instance.*EqDec' {} \; finds that there are too many files re-defining the same instances for deciding equality of e.g. PA's signature. This instance should be declared once, ideally along with PA itself.