let rec fuse i s r =  
  Trace.msg (Th.to_string i) "Fuse" r (Pretty.list Fact.pp_equal);
  let dom =
    List.fold_right
      (fun e ->
         let (x, _, _) = Fact.d_equal e in
           Set.union (use s x))
      r Set.empty
  in
  let eqs = ref Fact.Equalset.empty in
  let changed = ref Term.Set.empty in
  let s' = 
    Set.fold 
      (fun x acc ->
         try
           let (b, prf) = justification s x in     (* [prf |- x = b]. *)
           let (b', prfs) = norm i r b in          (* [prfs |- b = b']. *)
           let e' = Fact.mk_equal x b' (Fact.mk_rule "trans" (prf :: prfs)) in
             if is_var b' then 
               begin
                 eqs := Fact.Equalset.add e' !eqs;
                 restrict i x acc
               end 
             else 
               update (changed, eqs) i e' acc
         with
             Not_found -> acc)
      dom s
  in 
    (!changed, !eqs, s')



and update (changed, eqs) i e s =
  let  vareq e s = 
    let (x, y, prf1) = Fact.d_equal e in          (* [prf1 |- x = y]. *)
      eqs := Fact.Equalset.add e !eqs;
      try
        let (a, prf2) = justification s y in       (* [ prf2 |- y = a]. *)
          if y <<< x then
            restrict i x s
          else 
            let e' = Fact.mk_equal x a (Fact.mk_rule "trans" [prf1; prf2]) in
            let s' = restrict i y s in 
              changed := Term.Set.add x !changed;
              union i e' s'
      with
          Not_found -> 
            restrict i x s
  in
  let (x, b, prf1) = Fact.d_equal e in           (* [prf1 |- x = b]. *)
    if Term.eq x b then
      restrict i x s
    else if is_var b then
      vareq e s
    else
      try
        let y = inv s b in 
          if Term.eq x y then s else 
            let e' = Fact.mk_equal x y None in
              eqs := Fact.Equalset.add e' !eqs;
              if y <<< x then 
                restrict i x s 
              else 
                let s' = restrict i y s in
                  begin
                    changed := Term.Set.add x !changed;
                    union i e s'
                  end
      with
          Not_found -> 
            changed := Term.Set.add x !changed;
            union i e s