let name = 
  let v = Name.of_string "v" 
  and rho = Fact.mk_rule "extend" [] in
    fun i (b, s) ->
      let extend i b s = 
        let x = Term.mk_rename v None None in
        let e = Fact.mk_equal x b rho in
          Trace.msg (to_string i) "Ext" e Fact.pp_equal;
          (x, union i e s)
      in
        try
          (inv s b, s)
        with
            Not_found -> 
              extend i b s