(* type naif_indexing =
    (Cic.term * ((bool * Inference.equality) list)) list 
;; *)

type pos = Left | Right 
;;

let head_of_term =
  function 
    | Cic.Appl hd::tl -> hd
    | t -> t
;;

let index table eq =
  let (_,(_,l,r,ordering),_,_) = eq in
  let hl = head_of_term l in
  let hr = head_of_term r in
  let index x pos = 
    let x_entry = 
      try Hashtbl.find table x
      with Not_found -> [] in
      Hashtbl.replace table x (pos,eq)::x_entry in
  (match ordering with
    | Utils.Gt -> 
	index hl Left
    | Utils.Lt -> 
	index hr Right
    | _ -> index hl Left;
	index hr Right);
  table
;;

let demodulate_term env table cmp term =
  let hd_term = head_of_term term in
  let candidates = Hashtbl.find table hd_term in