+ (* rewrite_eq check if in table there an equation matching l=r;
+ used in subsumption and deep_eq. In deep_eq, we need to match
+ several times times w.r.t. the same table, hence we should refresh
+ the retrieved clauses, to avoid clashes of variables *)
+
+ let rewrite_eq ~refresh ~unify maxvar l r ty vl table =