sig
  type t = Term.t -> Term.t -> Jst.jst option
  val apply : Jst.Eqtrans.t -> Jst.Pred2.t -> Jst.Pred2.t
  val orelse : Jst.Pred2.t -> Jst.Pred2.t -> Jst.Pred2.t
  val inj : (Term.t -> Term.t -> bool) -> Jst.Pred2.t
  val trace : Trace.level -> string -> Jst.Pred2.t -> Jst.Pred2.t
end