diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
old mode 100755
new mode 100644
index cc88980b39..f5c7066c28
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -1050,12 +1050,22 @@ T pretty_fn<T>::pp_binder_block(buffer<name> const & names, expr const & type, b
     T r;
     if (m_binder_types || bi != binder_info())
         r += T(open_binder_string(bi, m_unicode));
-    for (name const & n : names) {
-        r += escape(n);
-        r += space();
-    }
-    if (m_binder_types) {
-        r += compose(colon(), nest(m_indent, compose(line(), pp_child(type, 0).fmt())));
+    if (bi.is_inst_implicit() && names.size() == 1 && names[0].is_anonymous()) {
+        // Prefer printing non-dependent instance implicit binder as `[foo]` rather than `[_ : foo]`.
+        // (Note: instance implicits always have `names.size() == 1`.)
+        r += pp_child(type, 0).fmt();
+    } else {
+        for (name const & n : names) {
+            if (n.is_anonymous()) {
+                r += T("_");
+            } else {
+                r += escape(n);
+            }
+            r += space();
+        }
+        if (m_binder_types) {
+            r += compose(colon(), nest(m_indent, compose(line(), pp_child(type, 0).fmt())));
+        }
     }
     if (m_binder_types || bi != binder_info())
         r += T(close_binder_string(bi, m_unicode));
@@ -1116,32 +1126,44 @@ static bool is_default_arrow(expr const & e) {
 }
 template<class T>
 auto pretty_fn<T>::pp_pi(expr const & e) -> result {
-    if (is_default_arrow(e)) {
-        result lhs = pp_child_at(binding_domain(e), get_arrow_prec(), expr_address::binding_type(e));
-        expr   b   = lift_free_vars(binding_body(e), 1);
-        address pb = expr_address::pi_body();
-        result rhs = is_pi(b) ? pp_at(b, pb) : pp_child_at(b, get_arrow_prec() - 1, pb);
-        T r   = group(lhs.fmt() + space() + mk_builtin_link(is_prop(b) ? "implies" : "function", m_unicode ? *g_arrow_n_fmt : *g_arrow_fmt) + line() + rhs.fmt());
-        return result(get_arrow_prec(), get_arrow_prec()-1, r);
-    } else {
-        expr b = e;
-        address adr;
-        buffer<subexpr> locals;
-        while (is_pi(b) && !is_default_arrow(b)) {
-            auto p = binding_body_fresh(b, true);
-            locals.push_back(mk_pair(p.second, cons(expr_coord::pi_var_type, adr)));
-            b = p.first;
-            adr = cons(expr_coord::pi_body, adr);
+    expr b = e;
+    address adr;
+    buffer<subexpr> locals;
+    while (is_pi(b)) {
+        auto p = binding_body_fresh(b, true);
+        if (is_default_arrow(b) && !(!is_prop(binding_domain(b)) && is_prop(p.first))) {
+            // Then this is an arrow that isn't from a Type to a Prop (we instead prefer forall notation in such cases)
+            if (locals.size() == 0) {
+                // Then we pretty print an arrow immediately
+                result lhs = pp_child_at(binding_domain(b), get_arrow_prec(), expr_address::binding_type(b));
+                b = p.first;
+                address pb = expr_address::pi_body();
+                result rhs = is_pi(b) ? pp_at(b, pb) : pp_child_at(b, get_arrow_prec() - 1, pb);
+                T r = group(lhs.fmt() + space() +  mk_builtin_link(is_prop(b) ? "implies" : "function", m_unicode ? *g_arrow_n_fmt : *g_arrow_fmt) + line() + rhs.fmt());
+                return result(get_arrow_prec(), get_arrow_prec()-1, r);
+            } else {
+                // Then we are done with the loop and pretty print the pi/forall
+                break;
+            }
         }
-        T r;
-        if (is_prop(b))
-            r = mk_builtin_link("forall", m_unicode ? *g_forall_n_fmt : *g_forall_fmt);
-        else
-            r = mk_builtin_link("pi", m_unicode ? *g_pi_n_fmt : *g_pi_fmt);
-        r += pp_binders(locals);
-        r += group(compose(comma(), nest(m_indent, compose(line(), pp_child_at(b, 0, adr).fmt()))));
-        return result(0, r);
+        expr local = p.second;
+        if (is_arrow(b)) {
+            // To let the user know this is a non-dependent pi we make the pp name for the local be anonymous,
+            // which is printed by `pp_binders` as '_'.
+            local = mk_local(binding_name(b), name(), binding_domain(b), binding_info(b));
+        }
+        locals.push_back(mk_pair(local, cons(expr_coord::pi_var_type, adr)));
+        b = p.first;
+        adr = cons(expr_coord::pi_body, adr);
     }
+    T r;
+    if (is_prop(b))
+        r = mk_builtin_link("forall", m_unicode ? *g_forall_n_fmt : *g_forall_fmt);
+    else
+        r = mk_builtin_link("pi", m_unicode ? *g_pi_n_fmt : *g_pi_fmt);
+    r += pp_binders(locals);
+    r += group(compose(comma(), nest(m_indent, compose(line(), pp_child_at(b, 0, adr).fmt()))));
+    return result(0, r);
 }
 
 static bool is_have(expr const & e) {
diff --git a/tests/lean/1917.lean.expected.out b/tests/lean/1917.lean.expected.out
index 563b52dbe5..b1139eae3b 100644
--- a/tests/lean/1917.lean.expected.out
+++ b/tests/lean/1917.lean.expected.out
@@ -7,6 +7,6 @@ The nested exception contains the failure state for the decreasing tactic.
 nested exception message:
 default_dec_tac failed
 state:
-foo : ℕ → false,
+foo : ∀ (_ : ℕ), false,
 x y : ℕ
 ⊢ y < x
diff --git a/tests/lean/584a.lean.expected.out b/tests/lean/584a.lean.expected.out
index e9343289d3..55599b17f4 100644
--- a/tests/lean/584a.lean.expected.out
+++ b/tests/lean/584a.lean.expected.out
@@ -1,5 +1,5 @@
-foo : Π (A : Type u_1) [H : inhabited A], A → A
-foo' : Π {A : Type u_1} [H : inhabited A] {x : A}, A
+foo : Π (A : Type u_1) [inhabited A], A → A
+foo' : Π {A : Type u_1} [inhabited A] {_ : A}, A
 foo ℕ 10 : ℕ
-def test : ∀ {A : Type u} [H : inhabited A], @foo' ℕ nat.inhabited (5 + 5) = 10 :=
+def test : ∀ {A : Type u} [inhabited A], @foo' ℕ nat.inhabited (5 + 5) = 10 :=
 λ {A : Type u} [H : inhabited A], @rfl ℕ (@foo' ℕ nat.inhabited (5 + 5))
diff --git a/tests/lean/634d.lean.expected.out b/tests/lean/634d.lean.expected.out
index 05560ab3a9..c7f2e0bc45 100644
--- a/tests/lean/634d.lean.expected.out
+++ b/tests/lean/634d.lean.expected.out
@@ -3,8 +3,8 @@ _root_.A : Type → Type
 A : Sort l → Sort l
 _root_.A.{1} : Type → Type
 P : B → B
-_root_.P : Π {n : ℕ}, ℕ → ℕ
+_root_.P : Π {_ : ℕ}, ℕ → ℕ
 P : B → B
 _root_.P.{1} : ?M_1 → ?M_1
 @P 2 : B → B
-@_root_.P.{1} ℕ : Π {n : ℕ}, ℕ → ℕ
+@_root_.P.{1} ℕ : Π {_ : ℕ}, ℕ → ℕ
diff --git a/tests/lean/652.lean.expected.out b/tests/lean/652.lean.expected.out
index f4402e127c..0b276d8587 100644
--- a/tests/lean/652.lean.expected.out
+++ b/tests/lean/652.lean.expected.out
@@ -1,6 +1,6 @@
-R : Π {b c : bool}, Prop
+R : Π {_ _ : bool}, Prop
 R2 : bool → bool → Prop
 R3 : bool → bool → Prop
-R4 : bool → Π {c : bool}, Prop
-R5 : Π {b c : bool}, Prop
-R6 : Π {b : bool}, bool → Prop
+R4 : bool → Π {_ : bool}, Prop
+R5 : Π {_ _ : bool}, Prop
+R6 : Π {_ : bool}, bool → Prop
diff --git a/tests/lean/as_is_leak_bug.lean.expected.out b/tests/lean/as_is_leak_bug.lean.expected.out
index 074366fefc..82fd0ef321 100644
--- a/tests/lean/as_is_leak_bug.lean.expected.out
+++ b/tests/lean/as_is_leak_bug.lean.expected.out
@@ -1,8 +1,8 @@
-def f : Π {α : Type} [_inst_1 : has_to_string α], α → string :=
+def f : Π {α : Type} [has_to_string α], α → string :=
 λ {α : Type} [_inst_1 : has_to_string α] (a : α), to_string a
-def g : Π {α : Type} [_inst_1 : has_to_string α], α → string :=
+def g : Π {α : Type} [has_to_string α], α → string :=
 λ {α : Type} [_inst_1 : has_to_string α], f
-def g' : Π {α : Type} [_inst_1 : has_to_string α], (α → string) × Type :=
+def g' : Π {α : Type} [has_to_string α], (α → string) × Type :=
 λ {α : Type} [_inst_1 : has_to_string α], (f, α)
-def h : Π {α : Type} [_inst_1 : has_to_string α], (α → string) × (α → string) × ((α → string) × Type) × Type :=
+def h : Π {α : Type} [has_to_string α], (α → string) × (α → string) × ((α → string) × Type) × Type :=
 λ {α : Type} [_inst_1 : has_to_string α], (f, g, g', α)
diff --git a/tests/lean/class_instance_param.lean.expected.out b/tests/lean/class_instance_param.lean.expected.out
index aa72cba00b..c7241c906e 100644
--- a/tests/lean/class_instance_param.lean.expected.out
+++ b/tests/lean/class_instance_param.lean.expected.out
@@ -1,7 +1,6 @@
-densely_ordered : Π (α : Type u_1) [_inst_1 : preorder α], Prop
+densely_ordered : Π (α : Type u_1) [preorder α], Prop
 densely_ordered.mk :
   ∀ {α : Type u_1} [_inst_1 : preorder α],
     (∀ (a c : α), a < c → (∃ (b : α), a < b ∧ b < c)) → densely_ordered α
 densely_ordered.dense :
-  ∀ {α : Type u_1} [_inst_1 : preorder α] [self : densely_ordered α] (a c : α),
-    a < c → (∃ (b : α), a < b ∧ b < c)
+  ∀ {α : Type u_1} [_inst_1 : preorder α] [densely_ordered α] (a c : α), a < c → (∃ (b : α), a < b ∧ b < c)
diff --git a/tests/lean/derive.lean.expected.out b/tests/lean/derive.lean.expected.out
index 9b895b510f..fbc2b0e0a8 100644
--- a/tests/lean/derive.lean.expected.out
+++ b/tests/lean/derive.lean.expected.out
@@ -1,9 +1,7 @@
 foo.has_reflect :
-  Π (α : Type) [a : has_reflect α] (β : Type) [a : has_reflect β] [a : reflected Type α] [a : reflected Type β],
+  Π (α : Type) [has_reflect α] (β : Type) [has_reflect β] [reflected Type α] [reflected Type β],
     has_reflect (foo α β)
 foo'.decidable_eq :
-  Π (α : Type u_1) [a : decidable_eq α] (β : Type u_1) [a : decidable_eq β] (n ᾰ : ℕ),
-    decidable_eq (foo' α β n ᾰ)
+  Π (α : Type u_1) [decidable_eq α] (β : Type u_1) [decidable_eq β] (n ᾰ : ℕ), decidable_eq (foo' α β n ᾰ)
 foo'.has_sizeof :
-  Π (α : Type u_1) [a : has_sizeof α] (β : Type u_1) [a : has_sizeof β] (n ᾰ : ℕ),
-    has_sizeof (foo' α β n ᾰ)
+  Π (α : Type u_1) [has_sizeof α] (β : Type u_1) [has_sizeof β] (n ᾰ : ℕ), has_sizeof (foo' α β n ᾰ)
diff --git a/tests/lean/elab6.lean.expected.out b/tests/lean/elab6.lean.expected.out
index ff4b1ada64..9789cd1256 100644
--- a/tests/lean/elab6.lean.expected.out
+++ b/tests/lean/elab6.lean.expected.out
@@ -1,10 +1,10 @@
 H : @transitive.{1} nat R
-@F.{u_1} ?M_1 : Π ⦃a : ?M_1⦄ {b : ?M_1}, ?M_1 → Π ⦃e : ?M_1⦄, ?M_1 → ?M_1 → ?M_1
-@F.{0} bool ?M_1 ?M_2 bool.tt : Π ⦃e : bool⦄, bool → bool → bool
+@F.{u_1} ?M_1 : Π ⦃_ : ?M_1⦄ {_ : ?M_1}, ?M_1 → Π ⦃_ : ?M_1⦄, ?M_1 → ?M_1 → ?M_1
+@F.{0} bool ?M_1 ?M_2 bool.tt : Π ⦃_ : bool⦄, bool → bool → bool
 @F.{0} bool ?M_1 ?M_2 bool.tt ?M_3 bool.tt : bool → bool
 @F.{0} bool ?M_1 ?M_2 bool.tt ?M_3 bool.tt bool.tt : bool
 H : @transitive.{1} nat R
-@F.{u_1} ?M_1 : Π ⦃a : ?M_1⦄ {b : ?M_1}, ?M_1 → Π ⦃e : ?M_1⦄, ?M_1 → ?M_1 → ?M_1
-@F.{0} bool ?M_1 ?M_2 bool.tt : Π ⦃e : bool⦄, bool → bool → bool
+@F.{u_1} ?M_1 : Π ⦃_ : ?M_1⦄ {_ : ?M_1}, ?M_1 → Π ⦃_ : ?M_1⦄, ?M_1 → ?M_1 → ?M_1
+@F.{0} bool ?M_1 ?M_2 bool.tt : Π ⦃_ : bool⦄, bool → bool → bool
 @F.{0} bool ?M_1 ?M_2 bool.tt ?M_3 bool.tt : bool → bool
 @F.{0} bool ?M_1 ?M_2 bool.tt ?M_3 bool.tt bool.tt : bool
diff --git a/tests/lean/elab9.lean.expected.out b/tests/lean/elab9.lean.expected.out
index 5a4b0acd8a..233b94366b 100644
--- a/tests/lean/elab9.lean.expected.out
+++ b/tests/lean/elab9.lean.expected.out
@@ -7,4 +7,4 @@
     Π [_inst_3 : has_add A],
       @eq A a (@has_add.add A _inst_3 (@has_zero.zero A _inst_2) (@has_zero.zero A _inst_2)) → A
 λ (a b : nat) (H : @gt nat nat.has_lt a b) [_inst_1 : has_lt nat], @has_lt.lt nat _inst_1 a b :
-  Π (a b : nat), @gt nat nat.has_lt a b → Π [_inst_1 : has_lt nat], Prop
+  Π (a b : nat), @gt nat nat.has_lt a b → Π [has_lt nat], Prop
diff --git a/tests/lean/elab_error_msgs.lean.expected.out b/tests/lean/elab_error_msgs.lean.expected.out
index ca9d05ce3c..01116eee9b 100644
--- a/tests/lean/elab_error_msgs.lean.expected.out
+++ b/tests/lean/elab_error_msgs.lean.expected.out
@@ -3,7 +3,7 @@ elab_error_msgs.lean:2:0: error: type mismatch at application
 term
   λ (ha : ?m_1) (hb : ?m_2) (hb : ?m_3[ha, hb]), ha
 has type
-  Π (ha : ?m_1) (hb : ?m_2), ?m_3[ha, hb] → ?m_1
+  ∀ (ha : ?m_1) (hb : ?m_2) (_ : ?m_3[ha, hb]), ?m_1
 but is expected to have type
   ?m_1 → ?m_2 → ?m_3
 Additional information:
diff --git a/tests/lean/error_pos.lean.expected.out b/tests/lean/error_pos.lean.expected.out
index 088d76770c..7f7c4e0568 100644
--- a/tests/lean/error_pos.lean.expected.out
+++ b/tests/lean/error_pos.lean.expected.out
@@ -16,7 +16,7 @@ error_pos.lean:11:36: error: type expected at
   B
 term has type
   A → Type
-λ (A : Type) (B : A → Type), ⁇ → true : Π (A : Type), (A → Type) → Prop
+λ (A : Type) (B : A → Type), ∀ (_ : ⁇), true : Π (A : Type), (A → Type) → Prop
 error_pos.lean:13:43: error: type expected at
   B
 term has type
diff --git a/tests/lean/extends_priority.lean.expected.out b/tests/lean/extends_priority.lean.expected.out
index f53ae8d42e..e1c9a79f7c 100644
--- a/tests/lean/extends_priority.lean.expected.out
+++ b/tests/lean/extends_priority.lean.expected.out
@@ -1,18 +1,18 @@
 @[instance, priority 100, reducible]
-def B.to_A : Π {α : Type} [self : B α], A α :=
+def B.to_A : Π {α : Type} [B α], A α :=
 λ (α : Type) [self : B α], [B.to_A self]
 @[instance, priority 37, reducible]
-def C.to_B : Π {α : Type} [self : C α], B α :=
+def C.to_B : Π {α : Type} [C α], B α :=
 λ (α : Type) [self : C α], [C.to_B self]
 @[instance, priority 100, reducible]
-def D.to_C : Π {α : Type} [self : D α], C α :=
+def D.to_C : Π {α : Type} [D α], C α :=
 λ (α : Type) [self : D α], [D.to_C self]
 @[instance, priority 100]
-def B'.to_A' : Π (α : Type) [self : B' α], A' α :=
+def B'.to_A' : Π (α : Type) [B' α], A' α :=
 λ (α : Type) [self : B' α], A'.mk
 @[instance, priority 37]
-def C'.to_B' : Π (α : Type) [self : C' α], B' α :=
+def C'.to_B' : Π (α : Type) [C' α], B' α :=
 λ (α : Type) [self : C' α], B'.mk
 @[instance, priority 100]
-def D'.to_C' : Π (α : Type) [self : D' α], C' α :=
+def D'.to_C' : Π (α : Type) [D' α], C' α :=
 λ (α : Type) [self : D' α], C'.mk
diff --git a/tests/lean/interactive/info.lean.expected.out b/tests/lean/interactive/info.lean.expected.out
index df20c51652..7291bf9311 100644
--- a/tests/lean/interactive/info.lean.expected.out
+++ b/tests/lean/interactive/info.lean.expected.out
@@ -5,5 +5,5 @@
 {"record":{"full-id":"bool.tt","source":,"state":"⊢ bool","type":"bool"},"response":"ok","seq_num":7}
 {"record":{"doc":"(trace) enable/disable tracing for the given module and submodules"},"response":"ok","seq_num":10}
 {"record":{"full-id":"list.cons","source":,"state":"⊢ list bool","type":"Π {T : Type}, T → list T → list T"},"response":"ok","seq_num":13}
-{"record":{"full-id":"has_append.append","source":,"state":"⊢ list bool","type":"Π {α : Type} [self : has_append α], α → α → α"},"response":"ok","seq_num":16}
+{"record":{"full-id":"has_append.append","source":,"state":"⊢ list bool","type":"Π {α : Type} [has_append α], α → α → α"},"response":"ok","seq_num":16}
 {"record":{"full-id":"id","source":,"type":"Π {α : Sort u}, α → α"},"response":"ok","seq_num":19}
diff --git a/tests/lean/let1.lean b/tests/lean/let1.lean
index cccbb7b45d..711c2894ed 100644
--- a/tests/lean/let1.lean
+++ b/tests/lean/let1.lean
@@ -12,6 +12,8 @@ prelude -- Correct version
 
 -- TODO(Leo): fix expected output as soon as elaborator starts #checking let-expression type again
 
+-- Note(kmill): some pretty printing oddities with forall since it's bool rather than Prop
+
 #check let bool                := Sort 0,
           and  (p q : bool)   := ∀ c : bool, (p → q → c) → c,
           infixl `∧`:25       := and,
diff --git a/tests/lean/let1.lean.expected.out b/tests/lean/let1.lean.expected.out
index 5de34178bb..ee391fc5f5 100644
--- a/tests/lean/let1.lean.expected.out
+++ b/tests/lean/let1.lean.expected.out
@@ -1,20 +1,20 @@
 let bool : Type := Prop,
     and : bool → bool → Prop := λ (p q : bool), Π (c : bool), (p → q → c) → c,
-    and_intro : Π (p q : bool), p → q → and p q :=
+    and_intro : Π (p q : bool), p → ∀ (_ : q), and p q :=
       λ (p q : bool) (H1 : p) (H2 : q) (c : bool) (H : p → q → c), H H1 H2,
     and_elim_left : Π (p q : bool), and p q → p := λ (p q : bool) (H : and p q), H p (λ (H1 : p) (H2 : q), H1),
     and_elim_right : Π (p q : bool), and p q → q := λ (p q : bool) (H : and p q), H q (λ (H1 : p) (H2 : q), H2)
 in and_intro :
   ∀ (p q : Prop), p → q → ∀ (c : Prop), (p → q → c) → c
-let1.lean:19:17: error: invalid let-expression, term
+let1.lean:21:17: error: invalid let-expression, term
   λ (p q : bool) (H1 : p) (H2 : q) (c : bool) (H : p → q → c), H H1 H2
 has type
   Π (p q : bool), p → q → Π (c : bool), (p → q → c) → c
 but is expected to have type
-  Π (p q : bool), p → q → and q p
+  Π (p q : bool), p → ∀ (_ : q), and q p
 let bool : Type := Prop,
     and : bool → bool → Prop := λ (p q : bool), Π (c : bool), (p → q → c) → c,
-    and_intro : Π (p q : bool), p → q → and q p := ⁇,
+    and_intro : Π (p q : bool), p → ∀ (_ : q), and q p := ⁇,
     and_elim_left : Π (p q : bool), and p q → p := λ (p q : bool) (H : and p q), H p (λ (H1 : p) (H2 : q), H1),
     and_elim_right : Π (p q : bool), and p q → q := λ (p q : bool) (H : and p q), H q (λ (H1 : p) (H2 : q), H2)
 in and_intro :
diff --git a/tests/lean/out_param_proj.lean.expected.out b/tests/lean/out_param_proj.lean.expected.out
index 935c77853d..8c41a7daa0 100644
--- a/tests/lean/out_param_proj.lean.expected.out
+++ b/tests/lean/out_param_proj.lean.expected.out
@@ -1,3 +1,3 @@
 @[instance, priority 100, reducible]
-def module.to_add_comm_group : Π {α : Type u} {β : Type v} {_inst_1 : ring α} [self : module α β], add_comm_group β :=
+def module.to_add_comm_group : Π {α : Type u} {β : Type v} {_inst_1 : ring α} [module α β], add_comm_group β :=
 λ {α : Type u} (β : Type v) {_inst_1 : ring α} [self : module α β], [module.to_add_comm_group self]
diff --git a/tests/lean/pp_forall.lean b/tests/lean/pp_forall.lean
new file mode 100644
index 0000000000..0abc392982
--- /dev/null
+++ b/tests/lean/pp_forall.lean
@@ -0,0 +1,36 @@
+variables (p q : Prop)
+#check p → q
+#check p → ℕ
+#check ℕ → p
+#check ℕ → ℕ
+#check ℕ → Prop
+#check ℕ → Type
+#check ∀ (n : ℕ), n > 0
+#check ∀ (n : ℕ), 1 = 2
+#check Π (n : ℕ), ℤ
+#check Π {n : ℕ}, ℤ
+#check Π (n : ℕ), fin n
+#check ∀ n : ℕ, ¬∃ x : ℕ, x ≠ x
+#check Π (m n : ℕ), ℤ
+#check Π (m n : ℕ), fin m
+#check Π (m n : ℕ), fin n
+#check ∀ (m n : ℕ), 1 = 2
+#check ∀ (m n : ℕ), m = 1
+#check ∀ (m n : ℕ), n = 1
+#check ∀ (m n : ℕ), m = n
+#check ∀ (m : ℕ) (h : p), q ∧ m = 1
+#check ∀ (m : ℕ) (h : p), q
+#check ∀ (h : p) (m : ℕ), q ∧ m = 1
+#check ∀ (h : p) (m : ℕ), q
+
+section
+-- A limitation due to use of relaxed weak head normal form:
+
+#check let Prop' := Prop, not' (p : Prop') := ¬ p in ∀ (p : Prop'), p → not' p
+-- shows ∀ (p : Prop') (_ : p), not' p
+
+abbreviation Prop' := Sort 0
+#check let not' (p : Prop') := ¬ p in ∀ (p : Prop'), p → not' p
+-- shows ∀ (p : Prop'), p → not' p
+
+end
diff --git a/tests/lean/pp_forall.lean.expected.out b/tests/lean/pp_forall.lean.expected.out
new file mode 100644
index 0000000000..1194567379
--- /dev/null
+++ b/tests/lean/pp_forall.lean.expected.out
@@ -0,0 +1,25 @@
+p → q : Prop
+p → ℕ : Type
+∀ (_ : ℕ), p : Prop
+ℕ → ℕ : Type
+ℕ → Prop : Type
+ℕ → Type : Type 1
+∀ (n : ℕ), n > 0 : Prop
+∀ (_ : ℕ), 1 = 2 : Prop
+ℕ → ℤ : Type
+Π {_ : ℕ}, ℤ : Type
+Π (n : ℕ), fin n : Type
+∀ (_ : ℕ), ¬∃ (x : ℕ), x ≠ x : Prop
+ℕ → ℕ → ℤ : Type
+Π (m : ℕ), ℕ → fin m : Type
+ℕ → Π (n : ℕ), fin n : Type
+∀ (_ _ : ℕ), 1 = 2 : Prop
+∀ (m _ : ℕ), m = 1 : Prop
+∀ (_ n : ℕ), n = 1 : Prop
+∀ (m n : ℕ), m = n : Prop
+∀ (m : ℕ), p → q ∧ m = 1 : Prop
+∀ (_ : ℕ), p → q : Prop
+p → ∀ (m : ℕ), q ∧ m = 1 : Prop
+p → ∀ (_ : ℕ), q : Prop
+let Prop' : Type := Prop, not' : Prop' → Prop := λ (p : Prop'), ¬p in ∀ (p : Prop') (_ : p), not' p : Prop
+let not' : Prop' → Prop := λ (p : Prop'), ¬p in ∀ (p : Prop'), p → not' p : Prop
diff --git a/tests/lean/pp_parens.lean b/tests/lean/pp_parens.lean
index 331eb00ff3..f16fd87e01 100644
--- a/tests/lean/pp_parens.lean
+++ b/tests/lean/pp_parens.lean
@@ -7,6 +7,7 @@ set_option pp.parens true
 #check [1,2,3]++[3,4,5]
 
 #check ∀ (x y z : ℤ), x - (-3) = -2 + x
+#check Π (x y : ℤ), {x : ℤ // x - (-3) = -2 + x}
 #check ∀ (p : ℕ → ℕ → Prop), p (1 + 2) 3
 #check ∀ (f : ℕ → ℕ → ℕ), f 2 (f 3 4 + 1) + 2 = f 1 2
 
diff --git a/tests/lean/pp_parens.lean.expected.out b/tests/lean/pp_parens.lean.expected.out
index 279b6cc61f..76686e50a5 100644
--- a/tests/lean/pp_parens.lean.expected.out
+++ b/tests/lean/pp_parens.lean.expected.out
@@ -1,7 +1,8 @@
 ((1 + (2 * 3)) + 4) : ℕ
 nat.add_assoc : ∀ (n m k : ℕ), (((n + m) + k) = (n + (m + k)))
 (([1, 2, 3]) ++ ([3, 4, 5])) : list ℕ
-∀ (x : ℤ), ℤ → ℤ → ((x - (-3)) = ((-2) + x)) : Prop
+∀ (x _ _ : ℤ), ((x - (-3)) = ((-2) + x)) : Prop
+ℤ → ℤ → {x // ((x - (-3)) = ((-2) + x))} : Type
 ∀ (p : ℕ → ℕ → Prop), p (1 + 2) 3 : Prop
 ∀ (f : ℕ → ℕ → ℕ), ((f 2 (f 3 4 + 1) + 2) = f 1 2) : Prop
 (set.univ = (⋃ (n : ℕ), {m : ℕ | (m < n)})) : Prop
diff --git a/tests/lean/pp_shadowed_const.lean.expected.out b/tests/lean/pp_shadowed_const.lean.expected.out
index 7686c56565..fc8e570331 100644
--- a/tests/lean/pp_shadowed_const.lean.expected.out
+++ b/tests/lean/pp_shadowed_const.lean.expected.out
@@ -1,7 +1,7 @@
 pp_shadowed_const.lean:1:55: error: don't know how to synthesize placeholder
 context:
 bool : ℕ
-⊢ _root_.bool → _root_.bool = _root_.bool
+⊢ ∀ (_ : _root_.bool), _root_.bool = _root_.bool
 def g : 1 == 1 → 1 == 1 :=
 λ (heq_1 : 1 == 1), heq_1.symm
 pp_shadowed_const.lean:7:39: error: don't know how to synthesize placeholder
diff --git a/tests/lean/pp_zero_bug.lean.expected.out b/tests/lean/pp_zero_bug.lean.expected.out
index efe231685b..02d780192b 100644
--- a/tests/lean/pp_zero_bug.lean.expected.out
+++ b/tests/lean/pp_zero_bug.lean.expected.out
@@ -1,2 +1,2 @@
-has_zero.zero : Π {α : Type u_1} [self : has_zero α], α
-has_zero.zero : Π [self : has_zero ℕ], ℕ
+has_zero.zero : Π {α : Type u_1} [has_zero α], α
+has_zero.zero : Π [has_zero ℕ], ℕ
diff --git a/tests/lean/struct_class.lean.expected.out b/tests/lean/struct_class.lean.expected.out
index 4c197e4115..a1ca840fc8 100644
--- a/tests/lean/struct_class.lean.expected.out
+++ b/tests/lean/struct_class.lean.expected.out
@@ -1,8 +1,8 @@
 @[class]
 structure point : Type u_1 → Type u_2 → Type (max u_1 u_2)
 fields:
-point.x : Π {A : Type u_1} (B : Type u_2) [self : point A B], A
-point.y : Π (A : Type u_1) {B : Type u_2} [self : point A B], B
+point.x : Π {A : Type u_1} (B : Type u_2) [point A B], A
+point.y : Π (A : Type u_1) {B : Type u_2} [point A B], B
 structure point2 : Type u_1 → Type u_2 → Type (max u_1 u_2)
 fields:
 point2.x : Π {A : Type u_1} {B : Type u_2}, point2 A B → A