let mk_cnstrnt x c j = 
  Trace.msg "fact" "Cnstrnt" (x, c) (Pretty.infix Term.pp "" Sign.pp);
  (x, c, j)