let rec nrm i r a = 
  let eqs = ref [] in
  let assoc x = function
    | [] -> x
    | e :: el -> 
        let (a, b, prf) = Fact.d_equal e in
          if Term.eq x a then 
            begin
              eqs := prf :: !eqs;
              b 
            end
          else 
            assoc x el
  in
  let b = Th.map i (fun x -> assoc x r) a in
    (b, !eqs)

and norm i r a =
  Trace.call "foo3" "Norm" a Term.pp;
  let (b, prfs) = nrm i r a in
    Trace.exit "foo3" "Norm" b Term.pp;
    (b, prfs)

and assoc x = function
  | [] -> x
  | e :: el -> 
      let (a, b, prf) = Fact.d_equal e in
        if Term.eq x a then 
          begin
            eqs := prf :: !eqs;
            b 
          end
        else 
          assoc x el

and eqs = ref []