@sorawee About egg and eqsat, I was wondering: don’t macros defeat the ‘compatiblity’ property of equality?

yes

context screws everything

In which case eqsat can’t apply to any thing that contains a macro, right?

(or at least macros are stoppers)

I think so, but I hope that there might be a trick to circumvent that