prerr_endline
("GOAL SUBSUMED BY: " ^ Equality.string_of_equality equality);
prerr_endline ("SUBST:" ^ Subst.ppsubst subst);
let (_,p,(ty,l,r,_),m,id) = Equality.open_equality equality in
let cicmenv = Subst.apply_subst_metasenv subst (m @ menv) in
let p =
prerr_endline
("GOAL SUBSUMED BY: " ^ Equality.string_of_equality equality);
prerr_endline ("SUBST:" ^ Subst.ppsubst subst);
let (_,p,(ty,l,r,_),m,id) = Equality.open_equality equality in
let cicmenv = Subst.apply_subst_metasenv subst (m @ menv) in
let p =