: S_Term = struct

  module L = Make(Term)
  include L

  let mk_pred t = make (Eq (t, Term.vrai) ) 
    
  let vrai = mk_pred Term.vrai
  let faux = mk_pred Term.faux

 let neg a = match view a with
   | Eq(t1, t2) when Term.equal t2 Term.faux -> 
       make (Eq (t1, Term.vrai))
   | Eq(t1, t2) when Term.equal t2 Term.vrai -> 
       make (Eq (t1, Term.faux))
   | _ -> L.neg a

(* let terms_of a = 
   let l = match view a with 
     | Eq (t1, t2) -> [t1; t2] 
     | Distinct (_, l) | Builtin (_, _, l) -> l 
   in
   List.fold_left Term.subterms Term.Set.empty l
*)

 module SS = Symbols.Set     
(* let vars_of a = 
   Term.Set.fold (fun t -> SS.union (Term.vars_of t)) (terms_of a) SS.empty
*)
end