+let in_index trie equality =
+ let _, _, (_, l, r, ordering), _, _ = equality in
+ let psl = path_strings_of_term 0 l
+ and psr = path_strings_of_term 0 r in
+ let meta_convertibility = Inference.meta_convertibility_eq equality in
+ let ok ps =
+ try
+ let set = PSTrie.find ps trie in
+ PosEqSet.exists (fun (p, e) -> meta_convertibility e) set
+ with Not_found ->
+ false
+ in
+ (List.exists ok psl) || (List.exists ok psr)
+;;
+
+