diff --git a/src/kernel/converter.cpp b/src/kernel/converter.cpp
index c7cf8399c..babbb7d82 100644
--- a/src/kernel/converter.cpp
+++ b/src/kernel/converter.cpp
@@ -571,13 +571,26 @@ struct default_converter : public converter {
         if (m_env.prop_proof_irrel()) {
             // Proof irrelevance support for Prop (aka Type.{0})
             auto tcs    = infer_type(c, t);
+            auto scs    = infer_type(c, s);
             expr t_type = tcs.first;
+            expr s_type = scs.first;
+            // remark: is_prop returns true only if t_type reducible to Prop.
+            // If t_type contains metavariables, then reduction can get stuck, and is_prop will return false.
             auto pcs    = is_prop(t_type, c);
             if (pcs.first) {
-                auto scs = infer_type(c, s);
-                auto dcs = is_def_eq(t_type, scs.first, c, jst);
+                auto dcs = is_def_eq(t_type, s_type, c, jst);
                 if (dcs.first)
                     return to_bcs(true, dcs.second + scs.second + pcs.second + tcs.second);
+            } else {
+                // If we can't stablish whether t_type is Prop, we try s_type.
+                pcs = is_prop(s_type, c);
+                if (pcs.first) {
+                    auto dcs = is_def_eq(t_type, s_type, c, jst);
+                    if (dcs.first)
+                        return to_bcs(true, dcs.second + scs.second + pcs.second + tcs.second);
+                }
+                // This procedure will miss the case where s_type and t_type cannot be reduced to Prop
+                // because they contain metavariables.
             }
         }
 
diff --git a/tests/lean/run/matrix2.lean b/tests/lean/run/matrix2.lean
new file mode 100644
index 000000000..aa615374f
--- /dev/null
+++ b/tests/lean/run/matrix2.lean
@@ -0,0 +1,15 @@
+import logic
+
+variable matrix.{l} : Type.{l} → Type.{l}
+variable same_dim {A : Type} : matrix A → matrix A → Prop
+variable add {A : Type} (m1 m2 : matrix A) {H : same_dim m1 m2} : matrix A
+
+theorem same_dim_eq_args {A : Type} {m1 m2 m1' m2' : matrix A} (H1 : m1 = m1') (H2 : m2 = m2') (H : same_dim m1 m2) : same_dim m1' m2' :=
+subst H1 (subst H2 H)
+
+theorem add_congr {A : Type} (m1 m2 m1' m2' : matrix A) (H1 : m1 = m1') (H2 : m2 = m2') (H : same_dim m1 m2) : @add A m1 m2 H = @add A m1' m2' (same_dim_eq_args H1 H2 H) :=
+have base : ∀ (H1 : m1 = m1) (H2 : m2 = m2), @add A m1 m2 H = @add A m1 m2 (eq_rec (eq_rec H H1) H2), from
+  assume H1 H2, rfl,
+have general : ∀ (H1 : m1 = m1') (H2 : m2 = m2'), @add A m1 m2 H = @add A m1' m2' (eq_rec (eq_rec H H1) H2), from
+  subst H1 (subst H2 base),
+general H1 H2