It is somewhat strange, but I haven’t really spent much time working on proof production or recording out of egraphs.