diff --git a/src/library/relation_manager.cpp b/src/library/relation_manager.cpp
index 8dacca1e4..b7dd74f9c 100644
--- a/src/library/relation_manager.cpp
+++ b/src/library/relation_manager.cpp
@@ -226,6 +226,10 @@ optional<std::tuple<name, name, unsigned>> get_trans_extra_info(environment cons
     }
 }
 
+bool is_subst_relation(environment const & env, name const & op) {
+    return rel_ext::get_state(env).m_subst_table.contains(op);
+}
+
 optional<name> get_refl_info(environment const & env, name const & op) {
     if (auto it = get_refl_extra_info(env, op))
         return optional<name>(std::get<0>(*it));
diff --git a/src/library/relation_manager.h b/src/library/relation_manager.h
index f1a6d14f1..74f694b29 100644
--- a/src/library/relation_manager.h
+++ b/src/library/relation_manager.h
@@ -41,6 +41,11 @@ optional<std::tuple<name, name, unsigned>> get_trans_extra_info(environment cons
 optional<name> get_refl_info(environment const & env, name const & op);
 optional<name> get_symm_info(environment const & env, name const & op);
 optional<name> get_trans_info(environment const & env, name const & op);
+bool is_subst_relation(environment const & env, name const & op);
+inline bool is_trans_relation(environment const & env, name const & op) { return static_cast<bool>(get_trans_info(env, op)); }
+inline bool is_symm_relation(environment const & env, name const & op) { return static_cast<bool>(get_symm_info(env, op)); }
+inline bool is_refl_relation(environment const & env, name const & op) { return static_cast<bool>(get_refl_info(env, op)); }
+
 void initialize_relation_manager();
 void finalize_relation_manager();
 }