diff --git a/src/library/tactic/congruence/congruence_closure.cpp b/src/library/tactic/congruence/congruence_closure.cpp
index a35d44c0cb..1b7739fd91 100644
--- a/src/library/tactic/congruence/congruence_closure.cpp
+++ b/src/library/tactic/congruence/congruence_closure.cpp
@@ -965,8 +965,17 @@ expr congruence_closure::mk_proof(expr const & lhs, expr const & rhs, expr const
             R = *is_refl_relation(lhs, a, b);
             flip = false;
         }
-        expr a_eq_b        = *get_eq_proof(a, b);
-        expr a_R_b         = lift_from_eq(m_ctx, R, a_eq_b);
+        expr a_R_b;
+        if (R == get_eq_name()) {
+            a_R_b        = *get_eq_proof(a, b);
+        } else if (R == get_heq_name()) {
+            a_R_b        = *get_heq_proof(a, b);
+        } else {
+            /* TODO(Leo): the following code assumes R is homogeneous.
+               We should add support arbitrary heterogenous reflexive relations. */
+            expr a_eq_b  = *get_eq_proof(a, b);
+            a_R_b        = lift_from_eq(m_ctx, R, a_eq_b);
+        }
         expr a_R_b_eq_true = mk_eq_true_intro(m_ctx, a_R_b);
         if (flip)
             return mk_eq_symm(m_ctx, a_R_b_eq_true);
diff --git a/tests/lean/run/cc4.lean b/tests/lean/run/cc4.lean
new file mode 100644
index 0000000000..4264ab4a77
--- /dev/null
+++ b/tests/lean/run/cc4.lean
@@ -0,0 +1,18 @@
+open tactic
+
+universe variables u
+
+constant vector : Type u → nat → Type (max 1 u)
+axiom app : Π {α : Type u} {n m : nat}, vector α m → vector α n → vector α (m+n)
+
+example (n1 n2 n3 : nat) (v1 w1 : vector nat n1) (w1' : vector nat n3) (v2 w2 : vector nat n2) :
+        n1 = n3 → v1 = w1 → w1 == w1' → v2 = w2 → app v1 v2 == app w1' w2 :=
+by cc
+
+example (n1 n2 n3 : nat) (v1 w1 : vector nat n1) (w1' : vector nat n3) (v2 w2 : vector nat n2) :
+        n1 == n3 → v1 = w1 → w1 == w1' → v2 == w2 → app v1 v2 == app w1' w2 :=
+by cc
+
+example (n1 n2 n3 : nat) (v1 w1 v : vector nat n1) (w1' : vector nat n3) (v2 w2 w : vector nat n2) :
+        n1 == n3 → v1 = w1 → w1 == w1' → v2 == w2 → app w1' w2 == app v w → app v1 v2 = app v w :=
+by cc