Lift Egglog ground prover to non-ground equations

[wisnesky]

Now that egglog's boolean EqSat(Theory, GroundTerm, GroundTerm) is exposed as a CQL prover, to lift it to full theorem proving it is necessary to choose between

boolean Eq(Theory t, Term t1, Term t2) 
 t1' = herbrandize(t1)
 t2' = herbrandize(t2)
 return EqSat(t U vars(t1) U vars(t2), t1', t2');

and

Eq(Theory t, Term t1, Term t2) 
 t1' = herbrandize(t1)
 t2' = herbrandize(t2)
 return EqSat(t U vars(t1) U vars(t2) U {true,false,eq,eq(x,x)=false,eq(t1',t2')=true}, true, false);

or something else entirely, to lift the current egglog prover. The second method is from unfailing knuth-bendix completion, and the first is "naive". egraphs-good/egglog#519