diff --git a/src/kernel/converter.cpp b/src/kernel/converter.cpp
index 79d8929d3..c3b850095 100644
--- a/src/kernel/converter.cpp
+++ b/src/kernel/converter.cpp
@@ -363,6 +363,13 @@ struct default_converter : public converter {
         }
     }
 
+    /** \brief Return true iff t is a constant named f_name or an application of the form (f_name a_1 ... a_k) */
+    bool is_app_of(expr t, name const & f_name) {
+        while (is_app(t))
+            t = app_fn(t);
+        return is_constant(t) && const_name(t) == f_name;
+    }
+
     /** Return true iff t is definitionally equal to s. */
     virtual bool is_def_eq(expr const & t, expr const & s, context & c, delayed_justification & jst) {
         check_system("is_definitionally_equal");
@@ -446,10 +453,21 @@ struct default_converter : public converter {
                 return true;
         }
 
-        if (m_env.proof_irrel()) {
-            // Proof irrelevance support
+        if (m_env.prop_proof_irrel()) {
+            // Proof irrelevance support for Prop/Bool (aka Type.{0})
             expr t_type = c.infer_type(t);
-            return is_prop(t_type, c) && is_def_eq(t_type, c.infer_type(s), c, jst);
+            if (is_prop(t_type, c) && is_def_eq(t_type, c.infer_type(s), c, jst))
+                return true;
+        }
+
+        list<name> const & cls_proof_irrel = m_env.cls_proof_irrel();
+        if (!is_nil(cls_proof_irrel)) {
+            // Proof irrelevance support for classes
+            expr t_type = whnf(c.infer_type(t), c);
+            if (std::any_of(cls_proof_irrel.begin(), cls_proof_irrel.end(),
+                            [&](name const & cls_name) { return is_app_of(t_type, cls_name); }) &&
+                is_def_eq(t_type, c.infer_type(s), c, jst))
+                return true;
         }
 
         return false;
diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp
index 6339bee74..f8be8950f 100644
--- a/src/kernel/environment.cpp
+++ b/src/kernel/environment.cpp
@@ -21,8 +21,10 @@ public:
     }
 };
 
-environment_header::environment_header(unsigned trust_lvl, bool proof_irrel, bool eta, bool impredicative, std::unique_ptr<normalizer_extension const> ext):
-    m_trust_lvl(trust_lvl), m_proof_irrel(proof_irrel), m_eta(eta), m_impredicative(impredicative), m_norm_ext(std::move(ext)) {}
+environment_header::environment_header(unsigned trust_lvl, bool prop_proof_irrel, bool eta, bool impredicative,
+                                       list<name> const & cls_proof_irrel, std::unique_ptr<normalizer_extension const> ext):
+    m_trust_lvl(trust_lvl), m_prop_proof_irrel(prop_proof_irrel), m_eta(eta), m_impredicative(impredicative),
+    m_cls_proof_irrel(cls_proof_irrel), m_norm_ext(std::move(ext)) {}
 
 environment_extension::~environment_extension() {}
 
@@ -45,12 +47,13 @@ bool environment_id::is_descendant(environment_id const & id) const {
 environment::environment(header const & h, environment_id const & ancestor, definitions const & d, name_set const & g, extensions const & exts):
     m_header(h), m_id(environment_id::mk_descendant(ancestor)), m_definitions(d), m_global_levels(g), m_extensions(exts) {}
 
-environment::environment(unsigned trust_lvl, bool proof_irrel, bool eta, bool impredicative):
-    environment(trust_lvl, proof_irrel, eta, impredicative, std::unique_ptr<normalizer_extension>(new noop_normalizer_extension()))
+environment::environment(unsigned trust_lvl, bool prop_proof_irrel, bool eta, bool impredicative, list<name> const & cls_proof_irrel):
+    environment(trust_lvl, prop_proof_irrel, eta, impredicative, cls_proof_irrel, std::unique_ptr<normalizer_extension>(new noop_normalizer_extension()))
 {}
 
-environment::environment(unsigned trust_lvl, bool proof_irrel, bool eta, bool impredicative, std::unique_ptr<normalizer_extension> ext):
-    m_header(std::make_shared<environment_header>(trust_lvl, proof_irrel, eta, impredicative, std::move(ext))),
+environment::environment(unsigned trust_lvl, bool prop_proof_irrel, bool eta, bool impredicative, list<name> const & cls_proof_irrel,
+                         std::unique_ptr<normalizer_extension> ext):
+    m_header(std::make_shared<environment_header>(trust_lvl, prop_proof_irrel, eta, impredicative, cls_proof_irrel, std::move(ext))),
     m_extensions(std::make_shared<environment_extensions const>())
 {}
 
diff --git a/src/kernel/environment.h b/src/kernel/environment.h
index 0804877fd..42e7fe852 100644
--- a/src/kernel/environment.h
+++ b/src/kernel/environment.h
@@ -43,18 +43,21 @@ class environment_header {
        >= 1 means do not check imported modules, and do not check macros
        with level less than the value of this field.
     */
-    unsigned m_trust_lvl; //!the given one.
-    bool m_proof_irrel;   //!< true if the kernel assumes proof irrelevance
-    bool m_eta;           //!< true if the kernel uses eta-reduction in convertability checks
-    bool m_impredicative; //!< true if the kernel should treat (universe level 0) as a impredicative Prop/Bool.
+    unsigned m_trust_lvl;     //!the given one.
+    bool m_prop_proof_irrel;  //!< true if the kernel assumes proof irrelevance for Bool/Type (aka Type(0))
+    bool m_eta;               //!< true if the kernel uses eta-reduction in convertability checks
+    bool m_impredicative;     //!< true if the kernel should treat (universe level 0) as a impredicative Prop/Bool.
+    list<name> m_cls_proof_irrel; //!< list of proof irrelevant classes, if we want Id types to be proof irrelevant, we the name 'Id' in this list.
     std::unique_ptr<normalizer_extension const> m_norm_ext;
     void dealloc();
 public:
-    environment_header(unsigned trust_lvl, bool proof_irrel, bool eta, bool impredicative, std::unique_ptr<normalizer_extension const> ext);
+    environment_header(unsigned trust_lvl, bool prop_proof_irrel, bool eta, bool impredicative,
+                       list<name> const & cls_proof_irrel, std::unique_ptr<normalizer_extension const> ext);
     unsigned trust_lvl() const { return m_trust_lvl; }
-    bool proof_irrel() const { return m_proof_irrel; }
+    bool prop_proof_irrel() const { return m_prop_proof_irrel; }
     bool eta() const { return m_eta; }
     bool impredicative() const { return m_impredicative; }
+    list<name> const & cls_proof_irrel() const { return m_cls_proof_irrel; }
     normalizer_extension const & norm_ext() const { return *(m_norm_ext.get()); }
 };
 
@@ -107,8 +110,10 @@ class environment {
     environment(header const & h, environment_id const & id, definitions const & d, name_set const & global_levels, extensions const & ext);
 
 public:
-    environment(unsigned trust_lvl = 0, bool proof_irrel = true, bool eta = true, bool impredicative = true);
-    environment(unsigned trust_lvl, bool proof_irrel, bool eta, bool impredicative, std::unique_ptr<normalizer_extension> ext);
+    environment(unsigned trust_lvl = 0, bool prop_proof_irrel = true, bool eta = true, bool impredicative = true,
+                list<name> const & cls_proof_irrel = list<name>());
+    environment(unsigned trust_lvl, bool prop_proof_irrel, bool eta, bool impredicative, list<name> const & cls_proof_irrel,
+                std::unique_ptr<normalizer_extension> ext);
     ~environment();
 
     /** \brief Return the environment unique identifier. */
@@ -120,8 +125,11 @@ public:
     /** \brief Return the trust level of this environment. */
     unsigned trust_lvl() const { return m_header->trust_lvl(); }
 
-    /** \brief Return true iff the environment assumes proof irrelevance */
-    bool proof_irrel() const { return m_header->proof_irrel(); }
+    /** \brief Return true iff the environment assumes proof irrelevance for Type.{0} (i.e., Bool) */
+    bool prop_proof_irrel() const { return m_header->prop_proof_irrel(); }
+
+    /** \brief Return the list of classes marked as proof irrelevant */
+    list<name> const & cls_proof_irrel() const { return m_header->cls_proof_irrel(); }
 
     /** \brief Return true iff the environment assumes Eta-reduction */
     bool eta() const { return m_header->eta(); }
diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp
index 925661d9b..a5d3566ca 100644
--- a/src/library/kernel_bindings.cpp
+++ b/src/library/kernel_bindings.cpp
@@ -993,7 +993,8 @@ DEFINE_LUA_LIST(certified_definition, push_certified_definition, to_certified_de
 DECL_UDATA(environment)
 static int environment_is_descendant(lua_State * L) { return push_boolean(L, to_environment(L, 1).is_descendant(to_environment(L, 2))); }
 static int environment_trust_lvl(lua_State * L) { return push_integer(L, to_environment(L, 1).trust_lvl()); }
-static int environment_proof_irrel(lua_State * L) { return push_boolean(L, to_environment(L, 1).proof_irrel()); }
+static int environment_prop_proof_irrel(lua_State * L) { return push_boolean(L, to_environment(L, 1).prop_proof_irrel()); }
+static int environment_cls_proof_irrel(lua_State * L) { return push_list_name(L, to_environment(L, 1).cls_proof_irrel()); }
 static int environment_eta(lua_State * L) { return push_boolean(L, to_environment(L, 1).eta()); }
 static int environment_impredicative(lua_State * L) { return push_boolean(L, to_environment(L, 1).impredicative()); }
 static int environment_add_global_level(lua_State * L) { return push_environment(L, to_environment(L, 1).add_global_level(to_name_ext(L, 2))); }
@@ -1003,13 +1004,13 @@ static int environment_get(lua_State * L) { return push_definition(L, to_environ
 static int environment_add(lua_State * L) { return push_environment(L, to_environment(L, 1).add(to_certified_definition(L, 2))); }
 static int environment_replace(lua_State * L) { return push_environment(L, to_environment(L, 1).replace(to_certified_definition(L, 2))); }
 static int mk_empty_environment(lua_State * L) {
-    unsigned trust_lvl = get_uint_named_param(L, 1, "trust_lvl", 0);
-    trust_lvl          = get_uint_named_param(L, 1, "trust_level", trust_lvl);
-    bool proof_irrel   = get_bool_named_param(L, 1, "proof_irrel", true);
-    proof_irrel   = get_bool_named_param(L, 1, "proof_irrelevance", proof_irrel);
-    bool eta           = get_bool_named_param(L, 1, "eta", true);
-    bool impredicative = get_bool_named_param(L, 1, "impredicative", true);
-    return push_environment(L, environment(trust_lvl, proof_irrel, eta, impredicative));
+    unsigned trust_lvl    = get_uint_named_param(L, 1, "trust_lvl", 0);
+    trust_lvl             = get_uint_named_param(L, 1, "trust_level", trust_lvl);
+    bool prop_proof_irrel = get_bool_named_param(L, 1, "prop_proof_irrel", true);
+    bool eta              = get_bool_named_param(L, 1, "eta", true);
+    bool impredicative    = get_bool_named_param(L, 1, "impredicative", true);
+    list<name> const & cls_proof_irrel = get_list_name_named_param(L, 1, "cls_proof_irrel", list<name>());
+    return push_environment(L, environment(trust_lvl, prop_proof_irrel, eta, impredicative, cls_proof_irrel));
 }
 static int environment_forget(lua_State * L) { return push_environment(L, to_environment(L, 1).forget()); }
 
@@ -1018,8 +1019,8 @@ static const struct luaL_Reg environment_m[] = {
     {"is_descendant",     safe_function<environment_is_descendant>},
     {"trust_lvl",         safe_function<environment_trust_lvl>},
     {"trust_level",       safe_function<environment_trust_lvl>},
-    {"proof_irrel",       safe_function<environment_proof_irrel>},
-    {"proof_irrelevance", safe_function<environment_proof_irrel>},
+    {"prop_proof_irrel",  safe_function<environment_prop_proof_irrel>},
+    {"cls_proof_irrel",   safe_function<environment_cls_proof_irrel>},
     {"eta",               safe_function<environment_eta>},
     {"impredicative",     safe_function<environment_impredicative>},
     {"add_global_level",  safe_function<environment_add_global_level>},
diff --git a/src/tests/kernel/environment.cpp b/src/tests/kernel/environment.cpp
index ab735f245..8857238c4 100644
--- a/src/tests/kernel/environment.cpp
+++ b/src/tests/kernel/environment.cpp
@@ -125,7 +125,7 @@ public:
 };
 
 static void tst3() {
-    environment env(0, true, true, true, std::unique_ptr<normalizer_extension>(new normalizer_extension_tst()));
+    environment env(0, true, true, true, list<name>(), std::unique_ptr<normalizer_extension>(new normalizer_extension_tst()));
     expr A = Const("A");
     expr x = Const("x");
     expr id = Const("id");
diff --git a/src/util/lua_named_param.cpp b/src/util/lua_named_param.cpp
index 9d017e1a6..532970545 100644
--- a/src/util/lua_named_param.cpp
+++ b/src/util/lua_named_param.cpp
@@ -125,5 +125,27 @@ name_set get_name_set_named_param(lua_State * L, int idx, char const * opt_name,
         return def_value;
     }
 }
+
+list<name> get_list_name_named_param(lua_State * L, int idx, char const * opt_name, list<name> const & def_value) {
+    if (lua_istable(L, idx)) {
+        push_string(L, opt_name);
+        lua_gettable(L, idx);
+        if (is_list_name(L, -1) || lua_istable(L, -1)) {
+            list<name> result = to_list_name_ext(L, -1);
+            lua_pop(L, 1);
+            return result;
+        } else if (lua_isnil(L, -1)) {
+            lua_pop(L, 1);
+            return def_value;
+        } else {
+            lua_pop(L, 1);
+            throw exception(sstream() << "field '" << opt_name << "' must be a list of names in table at arg #" << idx);
+        }
+    } else if (idx <= lua_gettop(L) && !lua_isnil(L, idx)) {
+        throw exception(sstream() << "arg #" << idx << " must be a table");
+    } else {
+        return def_value;
+    }
+}
 }
 
diff --git a/src/util/lua_named_param.h b/src/util/lua_named_param.h
index 411013521..e937d3152 100644
--- a/src/util/lua_named_param.h
+++ b/src/util/lua_named_param.h
@@ -19,4 +19,5 @@ unsigned get_uint_named_param(lua_State * L, int idx, char const * opt_name, uns
 optional<unsigned> get_opt_uint_named_param(lua_State * L, int idx, char const * opt_name,
                                             optional<unsigned> const & def_value = optional<unsigned>());
 name_set get_name_set_named_param(lua_State * L, int idx, char const * opt_name, name_set const & def_value = name_set());
+list<name> get_list_name_named_param(lua_State * L, int idx, char const * opt_name, list<name> const & def_value);
 }
diff --git a/tests/lua/env1.lua b/tests/lua/env1.lua
index 3b9e4d17a..fd91261b5 100644
--- a/tests/lua/env1.lua
+++ b/tests/lua/env1.lua
@@ -5,5 +5,5 @@ local env2 = env:add_global_level("U")
 assert(not env:is_global_level("U"))
 assert(env2:is_global_level("U"))
 assert(env:eta())
-assert(env:proof_irrel())
+assert(env:prop_proof_irrel())
 assert(env:impredicative())
diff --git a/tests/lua/env2.lua b/tests/lua/env2.lua
index f5a8556dd..70f71ff15 100644
--- a/tests/lua/env2.lua
+++ b/tests/lua/env2.lua
@@ -1,8 +1,7 @@
 assert(not empty_environment({eta=false}):eta())
 assert(empty_environment({eta=true}):eta())
-assert(not empty_environment({proof_irrel=false}):proof_irrel())
-assert(not empty_environment({proof_irrel=false}):proof_irrelevance())
-assert(empty_environment({proof_irrel=true}):proof_irrelevance())
+assert(not empty_environment({prop_proof_irrel=false}):prop_proof_irrel())
+assert(empty_environment({prop_proof_irrel=true}):prop_proof_irrel())
 assert(empty_environment({impredicative=true}):impredicative())
 assert(not empty_environment({impredicative=false}):impredicative())
 assert(empty_environment({trust_lvl=10}):trust_lvl() == 10)
diff --git a/tests/lua/env3.lua b/tests/lua/env3.lua
index 5727726f4..f16bd94ca 100644
--- a/tests/lua/env3.lua
+++ b/tests/lua/env3.lua
@@ -14,7 +14,7 @@ local t   = type_checker(env)
 assert(t:is_def_eq(p, q))
 assert(t:is_def_eq(And(p, q), And(q, p)))
 
-env = init(empty_environment({proof_irrel=false}))
+env = init(empty_environment({prop_proof_irrel=false}))
 t   = type_checker(env)
 assert(not t:is_def_eq(p, q))
 assert(not t:is_def_eq(And(p, q), And(q, p)))