+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
+;;