diff --git a/src/frontends/lean/frontend.cpp b/src/frontends/lean/frontend.cpp
index 799fb969a..b531c58af 100644
--- a/src/frontends/lean/frontend.cpp
+++ b/src/frontends/lean/frontend.cpp
@@ -170,10 +170,15 @@ struct lean_extension : public environment::extension {
                  f : Pi {A : Type} (a : A) {B : Type} (b : B), A    Pattern _ * _ *
                  g : Pi {A B : Type} (a : A) (b : B), A             Pattern _ _ * *
 
-       TODO(Leo): not implemented yet
+        Remark: we remove the explicit suffix at mark_implicit_arguments.
     */
     bool compatible_denotation(expr const & d1, expr const & d2) {
-        return get_implicit_arguments(d1) == get_implicit_arguments(d2);
+        auto imp1 = get_implicit_arguments(d1);
+        auto imp2 = get_implicit_arguments(d2);
+        auto it1  = std::find(imp1.begin(), imp1.end(), false);
+        auto it2  = std::find(imp2.begin(), imp2.end(), false);
+        for (; it1 != imp1.end() && it2 != imp2.end() && *it1 == *it2; ++it1, ++it2) {}
+        return it1 == imp1.end() && it2 == imp2.end();
     }
 
     /**
diff --git a/tests/lean/implicit4.lean b/tests/lean/implicit4.lean
new file mode 100644
index 000000000..e30be5195
--- /dev/null
+++ b/tests/lean/implicit4.lean
@@ -0,0 +1,8 @@
+Variable f {A : Type}     (a1 a2 : A) {B : Type} (b1 b2 : B) : A
+Variable g {A1 A2 : Type} (a1 : A1) (a2 : A2) {B : Type} (b : B) : A1
+Variable p (a1 a2 : Int)  {B : Type} (b1 b2 b3 : B) : B
+Variable h {A1 A2 : Type} (a1 : A1) (a2 : A2) (a3 : A2) : A1
+Infix ++ : f
+Infix ++ : g
+Infix ++ : p
+Infix ++ : h
\ No newline at end of file
diff --git a/tests/lean/implicit4.lean.expected.out b/tests/lean/implicit4.lean.expected.out
new file mode 100644
index 000000000..dfaa28674
--- /dev/null
+++ b/tests/lean/implicit4.lean.expected.out
@@ -0,0 +1,6 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: f
+  Assumed: g
+  Assumed: p
+  Assumed: h
diff --git a/tests/lean/implicit5.lean b/tests/lean/implicit5.lean
new file mode 100644
index 000000000..68c61dbc0
--- /dev/null
+++ b/tests/lean/implicit5.lean
@@ -0,0 +1,10 @@
+Variable f {A : Type} (a1 a2 : A) : A
+Variable g : Int -> Int -> Int
+Variable h : Int -> Int -> Real -> Int
+Variable p {A B : Type} (a1 a2 : A) (b : B) : A
+Infix ++ : f
+Infix ++ : g
+Infix ++ : h
+Infix ++ : p
+Variable p2 {A B : Type} (a1 a2 : A) (b : B) {C : Type} (c : C) : A
+Infix ++ : p2
diff --git a/tests/lean/implicit5.lean.expected.out b/tests/lean/implicit5.lean.expected.out
new file mode 100644
index 000000000..4abcbeb39
--- /dev/null
+++ b/tests/lean/implicit5.lean.expected.out
@@ -0,0 +1,7 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: f
+  Assumed: g
+  Assumed: h
+  Assumed: p
+  Assumed: p2