+let remove_index tree equality =
+ let _, _, (_, l, r, ordering), _, _ = equality in
+ match ordering with
+ | Utils.Gt -> DT.remove_index tree l (Utils.Left, equality)
+ | Utils.Lt -> DT.remove_index tree r (Utils.Right, equality)
+ | _ ->
+ let tree = DT.remove_index tree r (Utils.Right, equality) in
+ DT.remove_index tree l (Utils.Left, equality)
+
+let index tree equality =
+ let _, _, (_, l, r, ordering), _, _ = equality in
+ match ordering with
+ | Utils.Gt -> DT.index tree l (Utils.Left, equality)
+ | Utils.Lt -> DT.index tree r (Utils.Right, equality)
+ | _ ->
+ let tree = DT.index tree r (Utils.Right, equality) in
+ DT.index tree l (Utils.Left, equality)
+
+
+let in_index tree equality =
+ let _, _, (_, l, r, ordering), _, _ = equality in
+ let meta_convertibility (pos,equality') =
+ Inference.meta_convertibility_eq equality equality'
+ in
+ DT.in_index tree l meta_convertibility || DT.in_index tree r meta_convertibility
+