+let build_ens_for_sym_eq sym_eq_URI termlist =
+ let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph sym_eq_URI in
+ match obj with
+ | Cic.Constant (_, _, _, uris, _) ->
+ assert (List.length uris <= List.length termlist);
+ let rec aux = function
+ | [], tl -> [], tl
+ | (uri::uris), (term::tl) ->
+ let ens, args = aux (uris, tl) in
+ (uri, term)::ens, args
+ | _, _ -> assert false
+ in
+ aux (uris, termlist)
+ | _ -> assert false
+(* [(UriManager.uri_of_string *)
+(* "cic:/Coq/Init/Logic/Logic_lemmas/equality/A.var", ty); *)
+(* (UriManager.uri_of_string *)
+(* "cic:/Coq/Init/Logic/Logic_lemmas/equality/x.var", x); *)
+(* (UriManager.uri_of_string *)
+(* "cic:/Coq/Init/Logic/Logic_lemmas/equality/y.var", y)] *)
+;;
+
+