Module Lpo.TypedSTerm

type term = Logtk.TypedSTerm.t
val orient_lpo : term -> term -> Constraint.t

orient a b generates a constraint that is sufficient for a to be bigger than b in LPO orderings satisfying the constraints

val orient_lpo_list : (term * term) list -> Constraint.t list

Orient a list of pairs