make equiv be a worklist algorithm rather than a recursive one to avoid blowing the stack on large equalities