Module Jst.Pred2


module Pred2: sig  end
Justifying predicates over pair of terms.


type t = Term.t -> Term.t -> Jst.jst option
val apply : Jst.Eqtrans.t -> t -> t
Test predicate p on f(a).
Parameters:
f : Jst.Eqtrans.t
p : t
a : 'a
b : 'a
val orelse : t -> t -> t
Parameters:
p : t
q : t
a : 'a
b : 'b
val inj : (Term.t -> Term.t -> bool) -> t
Parameters:
? : Term.t -> Term.t -> bool
val trace : Trace.level -> string -> t -> t
Parameters:
lvl : Trace.level
name : string
? : t