overlay equations https://github.com/SkySkimmer/Coq-Equations hint-rw-local 13725