+let subsumption env target source =
+ let _, (ty, tl, tr, _), tmetas, _ = target
+ and _, (ty', sl, sr, _), smetas, _ = source in
+ if ty <> ty' then
+ false
+ else
+ let metasenv, context, ugraph = env in
+ let metasenv = metasenv @ tmetas @ smetas in
+ let names = names_of_context context in
+ let samesubst subst subst' =
+(* Printf.printf "samesubst:\nsubst: %s\nsubst': %s\n" *)
+(* (print_subst subst) (print_subst subst'); *)
+(* print_newline (); *)
+ let tbl = Hashtbl.create (List.length subst) in
+ List.iter (fun (m, (c, t1, t2)) -> Hashtbl.add tbl m (c, t1, t2)) subst;
+ List.for_all
+ (fun (m, (c, t1, t2)) ->
+ try
+ let c', t1', t2' = Hashtbl.find tbl m in
+ if (c = c') && (t1 = t1') && (t2 = t2') then true
+ else false
+ with Not_found ->
+ true)
+ subst'
+ in
+ let subsaux left right left' right' =
+ try
+ let subst, menv, ug = matching metasenv context left left' ugraph
+ and subst', menv', ug' = matching metasenv context right right' ugraph
+ in
+(* Printf.printf "left = right: %s = %s\n" *)
+(* (CicPp.pp left names) (CicPp.pp right names); *)
+(* Printf.printf "left' = right': %s = %s\n" *)
+(* (CicPp.pp left' names) (CicPp.pp right' names); *)
+ samesubst subst subst'
+ with e ->
+(* print_endline (Printexc.to_string e); *)
+ false
+ in
+ let res =
+ if subsaux tl tr sl sr then true
+ else subsaux tl tr sr sl
+ in
+ if res then (
+ Printf.printf "subsumption!:\ntarget: %s\nsource: %s\n"
+ (string_of_equality ~env target) (string_of_equality ~env source);
+ print_newline ();
+ );
+ res
+;;
+
+
+let extract_differing_subterms t1 t2 =
+ let module C = Cic in
+ let rec aux t1 t2 =
+ match t1, t2 with
+ | C.Appl l1, C.Appl l2 when (List.length l1) <> (List.length l2) ->
+ [(t1, t2)]
+ | C.Appl (h1::tl1), C.Appl (h2::tl2) ->
+ let res = List.concat (List.map2 aux tl1 tl2) in
+ if h1 <> h2 then
+ if res = [] then [(h1, h2)] else [(t1, t2)]
+ else
+ if List.length res > 1 then [(t1, t2)] else res
+ | t1, t2 ->
+ if t1 <> t2 then [(t1, t2)] else []
+ in
+ let res = aux t1 t2 in
+ match res with
+ | hd::[] -> Some hd
+ | _ -> None
+;;