One of the authors of this work apparently now works on supercompilers at Meta and open sourced some nice tools for equivalence checking based on graph rewriting [1] and constructive type theory [2]. If you're interested in that kind of thing I would recommend checking out his work:
[1]: https://github.com/ilya-klyuchnikov/mrsc
[2]: https://github.com/ilya-klyuchnikov/ttlite