A simple implementation of congruence closure, CongruenceClosure, which drives modifications to an arbitrary union-find ADT implementing the UnionFind trait.
Based on Nieuwenhuis and Oliveras Proof-producing Congruence Closure.
A minimal disjoint set forest implementation with dense usize nodes, DisjointSetForest, is also provided.