diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index 68c8491c1c..b388258239 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -20,6 +20,8 @@ namespace lean {
 static name g_llevel_curly(".{");
 static name g_lcurly("{");
 static name g_rcurly("}");
+static name g_ldcurly("⦃");
+static name g_rdcurly("⦄");
 static name g_lbracket("[");
 static name g_rbracket("]");
 static name g_colon(":");
@@ -47,11 +49,20 @@ binder_info parse_open_binder_info(parser & p) {
     if (p.curr_is_token(g_lcurly)) {
         check_in_section(p);
         p.next();
-        return mk_implicit_binder_info();
+        if (p.curr_is_token(g_lcurly)) {
+            p.next();
+            return mk_strict_implicit_binder_info();
+        } else {
+            return mk_implicit_binder_info();
+        }
     } else if (p.curr_is_token(g_lbracket)) {
         check_in_section(p);
         p.next();
         return mk_cast_binder_info();
+    } else if (p.curr_is_token(g_ldcurly)) {
+        check_in_section(p);
+        p.next();
+        return mk_strict_implicit_binder_info();
     } else {
         return binder_info();
     }
@@ -62,6 +73,13 @@ void parse_close_binder_info(parser & p, binder_info const & bi) {
         p.check_token_next(g_rcurly, "invalid declaration, '}' expected");
     } else if (bi.is_cast()) {
         p.check_token_next(g_rbracket, "invalid declaration, ']' expected");
+    } else if (bi.is_strict_implicit()) {
+        if (p.curr_is_token(g_lcurly)) {
+            p.next();
+            p.check_token_next(g_rdcurly, "invalid declaration, '}' expected");
+        } else {
+            p.check_token_next(g_rdcurly, "invalid declaration, '⦄' expected");
+        }
     }
 }
 
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 26daf87a9d..b114ac280c 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -348,14 +348,22 @@ public:
         expr f      = visit(app_fn(e));
         auto f_t    = ensure_fun(f);
         f           = f_t.first;
-        expr d_type = binding_domain(f_t.second);
+        expr f_type = f_t.second;
+        lean_assert(is_pi(f_type));
+        while (is_pi(f_type) && binding_info(f_type).is_strict_implicit()) {
+            tag g        = f.get_tag();
+            expr imp_arg = mk_meta(some_expr(binding_domain(f_type)), g);
+            f            = mk_app(f, imp_arg, g);
+            f_type       = whnf(instantiate(binding_body(f_type), imp_arg));
+        }
+        expr d_type = binding_domain(f_type);
         expr a      = visit_expecting_type_of(app_arg(e), d_type);
         expr a_type = instantiate_metavars(infer_type(a));
         expr r      = mk_app(f, a, e.get_tag());
-        app_delayed_justification j(m_env, r, f_t.second, a_type);
+        app_delayed_justification j(m_env, r, f_type, a_type);
         if (!m_tc.is_def_eq(a_type, d_type, j)) {
             // try coercions
-            optional<expr> c     = get_coercion(a_type, d_type, binding_info(f_t.second).is_cast());
+            optional<expr> c     = get_coercion(a_type, d_type, binding_info(f_type).is_cast());
             bool coercion_worked = false;
             expr new_a;
             if (c) {
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index e7f924b684..b3d380070d 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -396,6 +396,8 @@ static name g_rparen(")");
 static name g_llevel_curly(".{");
 static name g_lcurly("{");
 static name g_rcurly("}");
+static name g_ldcurly("⦃");
+static name g_rdcurly("⦄");
 static name g_lbracket("[");
 static name g_rbracket("]");
 static name g_add("+");
@@ -578,16 +580,29 @@ parameter parser::parse_binder() {
         return p;
     } else if (curr_is_token(g_lcurly)) {
         next();
-        auto p = parse_binder_core(mk_implicit_binder_info());
-        check_token_next(g_rcurly, "invalid binder, '}' expected");
-        return p;
+        if (curr_is_token(g_lcurly)) {
+            next();
+            auto p = parse_binder_core(mk_strict_implicit_binder_info());
+            check_token_next(g_rcurly, "invalid binder, '}' expected");
+            check_token_next(g_rcurly, "invalid binder, '}' expected");
+            return p;
+        } else {
+            auto p = parse_binder_core(mk_implicit_binder_info());
+            check_token_next(g_rcurly, "invalid binder, '}' expected");
+            return p;
+        }
     } else if (curr_is_token(g_lbracket)) {
         next();
         auto p = parse_binder_core(mk_cast_binder_info());
         check_token_next(g_rbracket, "invalid binder, ']' expected");
         return p;
+    } else if (curr_is_token(g_ldcurly)) {
+        next();
+        auto p = parse_binder_core(mk_strict_implicit_binder_info());
+        check_token_next(g_rdcurly, "invalid binder, '⦄' expected");
+        return p;
     } else {
-        throw parser_error("invalid binder, '(', '{', '[' or identifier expected", pos());
+        throw parser_error("invalid binder, '(', '{', '[', '{{', '⦃' or identifier expected", pos());
     }
 }
 
@@ -623,12 +638,23 @@ void parser::parse_binders_core(buffer<parameter> & r) {
         check_token_next(g_rparen, "invalid binder, ')' expected");
     } else if (curr_is_token(g_lcurly)) {
         next();
-        parse_binder_block(r, mk_implicit_binder_info());
-        check_token_next(g_rcurly, "invalid binder, '}' expected");
+        if (curr_is_token(g_lcurly)) {
+            next();
+            parse_binder_block(r, mk_strict_implicit_binder_info());
+            check_token_next(g_rcurly, "invalid binder, '}' expected");
+            check_token_next(g_rcurly, "invalid binder, '}' expected");
+        } else {
+            parse_binder_block(r, mk_implicit_binder_info());
+            check_token_next(g_rcurly, "invalid binder, '}' expected");
+        }
     } else if (curr_is_token(g_lbracket)) {
         next();
         parse_binder_block(r, mk_cast_binder_info());
         check_token_next(g_rbracket, "invalid binder, ']' expected");
+    } else if (curr_is_token(g_ldcurly)) {
+        next();
+        parse_binder_block(r, mk_strict_implicit_binder_info());
+        check_token_next(g_rdcurly, "invalid binder, '⦄' expected");
     } else {
         return;
     }
@@ -641,7 +667,7 @@ local_environment parser::parse_binders(buffer<parameter> & r) {
     unsigned old_sz = r.size();
     parse_binders_core(r);
     if (old_sz == r.size())
-        throw parser_error("invalid binder, '(', '{', '[' or identifier expected", pos());
+        throw parser_error("invalid binder, '(', '{', '[', '{{', '⦃' or identifier expected", pos());
     return local_environment(m_env);
 }
 
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index 3fbdffc8b0..c73d7b081d 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -57,7 +57,7 @@ token_table init_token_table() {
     std::pair<char const *, unsigned> builtin[] =
         {{"fun", 0}, {"Pi", 0}, {"let", 0}, {"in", 0}, {"have", 0}, {"show", 0}, {"by", 0}, {"then", 0},
          {"from", 0}, {"(", g_max_prec}, {")", 0}, {"{", g_max_prec}, {"}", 0}, {"_", g_max_prec},
-         {"[", g_max_prec}, {"]", 0}, {".{", 0}, {"Type", g_max_prec}, {"|", 0}, {"with", 0},
+         {"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0}, {"Type", g_max_prec}, {"|", 0}, {"with", 0},
          {"...", 0}, {",", 0}, {".", 0}, {":", 0}, {"calc", 0}, {":=", 0}, {"--", 0}, {"#", 0},
          {"(*", 0}, {"(--", 0}, {"proof", 0}, {"qed", 0}, {"@", 0},
          {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {nullptr, 0}};
diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index 838c0b15f3..ef27517314 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -149,7 +149,11 @@ void expr_app::dealloc(buffer<expr_cell*> & todelete) {
 static unsigned dec(unsigned k) { return k == 0 ? 0 : k - 1; }
 
 bool operator==(binder_info const & i1, binder_info const & i2) {
-    return i1.is_implicit() == i2.is_implicit() && i1.is_cast() == i2.is_cast() && i1.is_contextual() == i2.is_contextual();
+    return
+        i1.is_implicit() == i2.is_implicit() &&
+        i1.is_cast() == i2.is_cast() &&
+        i1.is_contextual() == i2.is_contextual() &&
+        i1.is_strict_implicit() == i2.is_strict_implicit();
 }
 
 // Expr binders (Lambda, Pi)
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index 0e7e8dd73b..d9b5c49cc4 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -241,18 +241,21 @@ public:
    is only used for elaboration.
 */
 class binder_info {
-    unsigned m_implicit:1;   //! if true, binder argument is an implicit argument
-    unsigned m_cast:1;       //! if true, binder argument is a target for using cast
-    unsigned m_contextual:1; //! if true, binder argument is assumed to be part of the context, and may be argument for metavariables.
+    unsigned m_implicit:1;        //! if true, binder argument is an implicit argument
+    unsigned m_cast:1;            //! if true, binder argument is a target for using cast
+    unsigned m_contextual:1;      //! if true, binder argument is assumed to be part of the context, and may be argument for metavariables.
+    unsigned m_strict_implicit:1; //! if true, binder argument is assumed to be a strict implicit argument
 public:
-    binder_info(bool implicit = false, bool cast = false, bool contextual = true):
-        m_implicit(implicit), m_cast(cast), m_contextual(contextual) {}
+    binder_info(bool implicit = false, bool cast = false, bool contextual = true, bool strict_implicit = false):
+        m_implicit(implicit), m_cast(cast), m_contextual(contextual), m_strict_implicit(strict_implicit) {}
     bool is_implicit() const { return m_implicit; }
     bool is_cast() const { return m_cast; }
     bool is_contextual() const { return m_contextual; }
+    bool is_strict_implicit() const { return m_strict_implicit; }
 };
 
 inline binder_info mk_implicit_binder_info() { return binder_info(true); }
+inline binder_info mk_strict_implicit_binder_info() { return binder_info(false, false, true, true); }
 inline binder_info mk_cast_binder_info() { return binder_info(false, true); }
 inline binder_info mk_contextual_info(bool f) { return binder_info(false, false, f); }
 
diff --git a/src/kernel/formatter.cpp b/src/kernel/formatter.cpp
index df3da5eac7..3c6d60f352 100644
--- a/src/kernel/formatter.cpp
+++ b/src/kernel/formatter.cpp
@@ -134,6 +134,8 @@ struct print_expr_fn {
                 out() << "[";
             else if (!binding_info(e).is_contextual())
                 out() << "[[";
+            else if (binding_info(e).is_strict_implicit())
+                out() << "{{";
             else
                 out() << "(";
             out() << n << " : ";
@@ -144,6 +146,8 @@ struct print_expr_fn {
                 out() << "]";
             else if (!binding_info(e).is_contextual())
                 out() << "]]";
+            else if (binding_info(e).is_strict_implicit())
+                out() << "}}";
             else
                 out() << ")";
             e = p.first;
diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp
index c2ebd39655..7a4e675a3d 100644
--- a/src/library/kernel_bindings.cpp
+++ b/src/library/kernel_bindings.cpp
@@ -275,17 +275,21 @@ static int mk_binder_info(lua_State * L) {
         return push_binder_info(L, binder_info(lua_toboolean(L, 1)));
     else if (nargs == 2)
         return push_binder_info(L, binder_info(lua_toboolean(L, 1), lua_toboolean(L, 2)));
-    else
+    else if (nargs == 3)
         return push_binder_info(L, binder_info(lua_toboolean(L, 1), lua_toboolean(L, 2), lua_toboolean(L, 3)));
+    else
+        return push_binder_info(L, binder_info(lua_toboolean(L, 1), lua_toboolean(L, 2), lua_toboolean(L, 3), lua_toboolean(L, 4)));
 }
 static int binder_info_is_implicit(lua_State * L) { return push_boolean(L, to_binder_info(L, 1).is_implicit()); }
 static int binder_info_is_cast(lua_State * L) { return push_boolean(L, to_binder_info(L, 1).is_cast()); }
 static int binder_info_is_contextual(lua_State * L) { return push_boolean(L, to_binder_info(L, 1).is_contextual()); }
+static int binder_info_is_strict_implicit(lua_State * L) { return push_boolean(L, to_binder_info(L, 1).is_strict_implicit()); }
 static const struct luaL_Reg binder_info_m[] = {
-    {"__gc",            binder_info_gc},
-    {"is_implicit",     safe_function<binder_info_is_implicit>},
-    {"is_cast",         safe_function<binder_info_is_cast>},
-    {"is_contextual",   safe_function<binder_info_is_contextual>},
+    {"__gc",               binder_info_gc},
+    {"is_implicit",        safe_function<binder_info_is_implicit>},
+    {"is_cast",            safe_function<binder_info_is_cast>},
+    {"is_contextual",      safe_function<binder_info_is_contextual>},
+    {"is_strict_implicit", safe_function<binder_info_is_strict_implicit>},
     {0, 0}
 };
 static void open_binder_info(lua_State * L) {
diff --git a/src/library/kernel_serializer.cpp b/src/library/kernel_serializer.cpp
index aa8f974d7d..f5fb80e9a2 100644
--- a/src/library/kernel_serializer.cpp
+++ b/src/library/kernel_serializer.cpp
@@ -119,13 +119,17 @@ static expr read_macro_definition(deserializer & d, unsigned num, expr const * a
 serializer & operator<<(serializer & s, binder_info const & i) {
     s.write_bool(i.is_implicit());
     s.write_bool(i.is_cast());
+    s.write_bool(i.is_contextual());
+    s.write_bool(i.is_strict_implicit());
     return s;
 }
 
 static binder_info read_binder_info(deserializer & d) {
-    bool imp = d.read_bool();
-    bool cast = d.read_bool();
-    return binder_info(imp, cast);
+    bool imp   = d.read_bool();
+    bool cast  = d.read_bool();
+    bool ctx   = d.read_bool();
+    bool s_imp = d.read_bool();
+    return binder_info(imp, cast, ctx, s_imp);
 }
 
 class expr_serializer : public object_serializer<expr, expr_hash_alloc, expr_eqp> {
diff --git a/tests/lean/run/e5.lean b/tests/lean/run/e5.lean
new file mode 100644
index 0000000000..8c18c2198f
--- /dev/null
+++ b/tests/lean/run/e5.lean
@@ -0,0 +1,69 @@
+definition Bool [inline] := Type.{0}
+
+definition false : Bool := ∀x : Bool, x
+check false
+
+theorem false_elim (C : Bool) (H : false) : C
+:= H C
+
+definition eq {A : Type} (a b : A)
+:= ∀ P : A → Bool, P a → P b
+
+check eq
+
+infix `=` 50 := eq
+
+theorem refl {A : Type} (a : A) : a = a
+:= λ P H, H
+
+definition true : Bool
+:= false = false
+
+theorem trivial : true
+:= refl false
+
+theorem subst {A : Type} {P : A -> Bool} {a b : A} (H1 : a = b) (H2 : P a) : P b
+:= H1 _ H2
+
+theorem symm {A : Type} {a b : A} (H : a = b) : b = a
+:= subst H (refl a)
+
+theorem trans {A : Type} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c
+:= subst H2 H1
+
+inductive nat : Type :=
+| zero : nat
+| succ : nat → nat
+
+print "using strict implicit arguments"
+abbreviation symmetric {A : Type} (R : A → A → Bool) := ∀ ⦃a b⦄, R a b → R b a
+
+check symmetric
+variable p : nat → nat → Bool
+check symmetric p
+axiom H1 : symmetric p
+axiom H2 : p zero (succ zero)
+check H1
+check H1 H2
+
+print "------------"
+print "using implicit arguments"
+abbreviation symmetric2 {A : Type} (R : A → A → Bool) := ∀ {a b}, R a b → R b a
+check symmetric2
+check symmetric2 p
+axiom H3 : symmetric2 p
+axiom H4 : p zero (succ zero)
+check H3
+check H3 H4
+
+print "-----------------"
+print "using strict implicit arguments (ASCII notation)"
+abbreviation symmetric3 {A : Type} (R : A → A → Bool) := ∀ {{a b}}, R a b → R b a
+
+check symmetric3
+check symmetric3 p
+axiom H5 : symmetric3 p
+axiom H6 : p zero (succ zero)
+check H5
+check H5 H6
+