It’s an egraph that supports well-scoped alpha aware binders.