let o = Order.compare_terms l r in
Terms.Equation (l, r, ty, o)
let o = Order.compare_terms l r in
Terms.Equation (l, r, ty, o)
in
let proof = Terms.Exact proofterm in
fresh_unit_clause maxvar (0, lit, varlist, proof)
in
let proof = Terms.Exact proofterm in
fresh_unit_clause maxvar (0, lit, varlist, proof)