diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 42c7db1efa..5058da03a6 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -50,7 +50,7 @@ reserve infix ` ≤ `:50
 reserve infix ` < `:50
 reserve infix ` >= `:50
 reserve infix ` ≥ `:50
-reserve infix ` > `:50
+ reserve infix ` > `:50
 
 /- boolean operations -/
 
@@ -205,8 +205,8 @@ constant Quot.ind {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop}
 -/
 init_quot
 
-inductive Heq {α : Sort u} (a : α) : ∀ {β : Sort u}, β → Prop
-| refl : Heq a
+inductive HEq {α : Sort u} (a : α) : ∀ {β : Sort u}, β → Prop
+| refl : HEq a
 
 structure Prod (α : Type u) (β : Type v) :=
 (fst : α) (snd : β)
@@ -242,14 +242,14 @@ h₂ ▸ h₁
 theorem Eq.symm {α : Sort u} {a b : α} (h : a = b) : b = a :=
 h ▸ rfl
 
-infix `~=` := Heq
-infix `≅` := Heq
+infix `~=` := HEq
+infix `≅` := HEq
 
-@[matchPattern] def Heq.rfl {α : Sort u} {a : α} : a ≅ a := Heq.refl a
+@[matchPattern] def HEq.rfl {α : Sort u} {a : α} : a ≅ a := HEq.refl a
 
-theorem eqOfHeq {α : Sort u} {a a' : α} (h : a ≅ a') : a = a' :=
-have ∀ (α' : Sort u) (a' : α') (h₁ : @Heq α a α' a') (h₂ : α = α'), (Eq.recOn h₂ a : α') = a' :=
-  fun (α' : Sort u) (a' : α') (h₁ : @Heq α a α' a') => Heq.recOn h₁ (fun (h₂ : α = α) => rfl);
+theorem eqOfHEq {α : Sort u} {a a' : α} (h : a ≅ a') : a = a' :=
+have ∀ (α' : Sort u) (a' : α') (h₁ : @HEq α a α' a') (h₂ : α = α'), (Eq.recOn h₂ a : α') = a' :=
+  fun (α' : Sort u) (a' : α') (h₁ : @HEq α a α' a') => HEq.recOn h₁ (fun (h₂ : α = α) => rfl);
 show (Eq.ndrecOn (Eq.refl α) a : α) = a' from
   this α a' h (Eq.refl α)
 
@@ -659,10 +659,10 @@ fun h₁ => h (h₁.symm)
 theorem falseOfNe : a ≠ a → False := Ne.irrefl
 
 theorem neFalseOfSelf : p → p ≠ False :=
-fun (hp : p) (Heq : p = False) => Heq ▸ hp
+fun (hp : p) (h : p = False) => h ▸ hp
 
 theorem neTrueOfNot : ¬p → p ≠ True :=
-fun (hnp : ¬p) (Heq : p = True) => (Heq ▸ hnp) trivial
+fun (hnp : ¬p) (h : p = True) => (h ▸ hnp) trivial
 
 theorem trueNeFalse : ¬True = False :=
 neFalseOfSelf trivial
@@ -680,46 +680,46 @@ section
 variables {α β φ : Sort u} {a a' : α} {b b' : β} {c : φ}
 
 @[elabAsEliminator]
-theorem Heq.ndrec.{u1, u2} {α : Sort u2} {a : α} {C : ∀ {β : Sort u2}, β → Sort u1} (m : C a) {β : Sort u2} {b : β} (h : a ≅ b) : C b :=
-@Heq.rec α a (fun β b _ => C b) m β b h
+theorem HEq.ndrec.{u1, u2} {α : Sort u2} {a : α} {C : ∀ {β : Sort u2}, β → Sort u1} (m : C a) {β : Sort u2} {b : β} (h : a ≅ b) : C b :=
+@HEq.rec α a (fun β b _ => C b) m β b h
 
 @[elabAsEliminator]
-theorem Heq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {C : ∀ {β : Sort u2}, β → Sort u1} {β : Sort u2} {b : β} (h : a ≅ b) (m : C a) : C b :=
-@Heq.rec α a (fun β b _ => C b) m β b h
+theorem HEq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {C : ∀ {β : Sort u2}, β → Sort u1} {β : Sort u2} {b : β} (h : a ≅ b) (m : C a) : C b :=
+@HEq.rec α a (fun β b _ => C b) m β b h
 
-theorem Heq.elim {α : Sort u} {a : α} {p : α → Sort v} {b : α} (h₁ : a ≅ b) (h₂ : p a) : p b :=
-Eq.recOn (eqOfHeq h₁) h₂
+theorem HEq.elim {α : Sort u} {a : α} {p : α → Sort v} {b : α} (h₁ : a ≅ b) (h₂ : p a) : p b :=
+Eq.recOn (eqOfHEq h₁) h₂
 
-theorem Heq.subst {p : ∀ (T : Sort u), T → Prop} (h₁ : a ≅ b) (h₂ : p α a) : p β b :=
-Heq.ndrecOn h₁ h₂
+theorem HEq.subst {p : ∀ (T : Sort u), T → Prop} (h₁ : a ≅ b) (h₂ : p α a) : p β b :=
+HEq.ndrecOn h₁ h₂
 
-theorem Heq.symm (h : a ≅ b) : b ≅ a :=
-Heq.ndrecOn h (Heq.refl a)
+theorem HEq.symm (h : a ≅ b) : b ≅ a :=
+HEq.ndrecOn h (HEq.refl a)
 
 theorem heqOfEq (h : a = a') : a ≅ a' :=
-Eq.subst h (Heq.refl a)
+Eq.subst h (HEq.refl a)
 
-theorem Heq.trans (h₁ : a ≅ b) (h₂ : b ≅ c) : a ≅ c :=
-Heq.subst h₂ h₁
+theorem HEq.trans (h₁ : a ≅ b) (h₂ : b ≅ c) : a ≅ c :=
+HEq.subst h₂ h₁
 
-theorem heqOfHeqOfEq (h₁ : a ≅ b) (h₂ : b = b') : a ≅ b' :=
-Heq.trans h₁ (heqOfEq h₂)
+theorem heqOfHEqOfEq (h₁ : a ≅ b) (h₂ : b = b') : a ≅ b' :=
+HEq.trans h₁ (heqOfEq h₂)
 
-theorem heqOfEqOfHeq (h₁ : a = a') (h₂ : a' ≅ b) : a ≅ b :=
-Heq.trans (heqOfEq h₁) h₂
+theorem heqOfEqOfHEq (h₁ : a = a') (h₂ : a' ≅ b) : a ≅ b :=
+HEq.trans (heqOfEq h₁) h₂
 
-def typeEqOfHeq (h : a ≅ b) : α = β :=
-Heq.ndrecOn h (Eq.refl α)
+def typeEqOfHEq (h : a ≅ b) : α = β :=
+HEq.ndrecOn h (Eq.refl α)
 end
 
-theorem eqRecHeq {α : Sort u} {φ : α → Sort v} : ∀ {a a' : α} (h : a = a') (p : φ a), (Eq.recOn h p : φ a') ≅ p
-| a, _, rfl, p => Heq.refl p
+theorem eqRecHEq {α : Sort u} {φ : α → Sort v} : ∀ {a a' : α} (h : a = a') (p : φ a), (Eq.recOn h p : φ a') ≅ p
+| a, _, rfl, p => HEq.refl p
 
-theorem ofHeqTrue {a : Prop} (h : a ≅ True) : a :=
-ofEqTrue (eqOfHeq h)
+theorem ofHEqTrue {a : Prop} (h : a ≅ True) : a :=
+ofEqTrue (eqOfHEq h)
 
-theorem castHeq : ∀ {α β : Sort u} (h : α = β) (a : α), cast h a ≅ a
-| α, _, rfl, a => Heq.refl a
+theorem castHEq : ∀ {α β : Sort u} (h : α = β) (a : α), cast h a ≅ a
+| α, _, rfl, a => HEq.refl a
 
 variables {a b c d : Prop}
 
@@ -1385,9 +1385,9 @@ Quot.rec f (fun a b h => Subsingleton.elim _ (f b)) q
 protected def hrecOn
    (q : Quot r) (f : ∀ a, β (Quot.mk r a)) (c : ∀ (a b : α) (p : r a b), f a ≅ f b) : β q :=
 Quot.recOn q f $
-  fun a b p => eqOfHeq $
-    have p₁ : (Eq.rec (f a) (sound p) : β (Quot.mk r b)) ≅ f a := eqRecHeq (sound p) (f a);
-    Heq.trans p₁ (c a b p)
+  fun a b p => eqOfHEq $
+    have p₁ : (Eq.rec (f a) (sound p) : β (Quot.mk r b)) ≅ f a := eqRecHEq (sound p) (f a);
+    HEq.trans p₁ (c a b p)
 
 end
 end Quot
diff --git a/src/Init/WF.lean b/src/Init/WF.lean
index 63d1317b3e..1d1e1200af 100644
--- a/src/Init/WF.lean
+++ b/src/Init/WF.lean
@@ -233,13 +233,13 @@ Acc.ndrecOn aca $ fun (xa aca) (iha : ∀ y, r y xa → ∀ (b : β y), Acc (Lex
                            (∀ (y : β xa), s xa y xb → Acc (Lex r s) ⟨xa, y⟩) →
                            Lex r s p ⟨xa, xb⟩ → ∀ (b₁ : β a), s a b₁ b₂ → b₂ ≅ xb → Acc (Lex r s) ⟨a, b₁⟩
               from Eq.subst Eq₂ $ fun xb acb ihb lt b₁ h Eq₃ =>
-                have newEq₃ : b₂ = xb from eqOfHeq Eq₃;
+                have newEq₃ : b₂ = xb from eqOfHEq Eq₃;
                 have aux : (∀ (y : β a), s a y xb → Acc (Lex r s) ⟨a, y⟩) →
                            ∀ (b₁ : β a), s a b₁ b₂ → Acc (Lex r s) ⟨a, b₁⟩
                 from Eq.subst newEq₃ (fun ihb b₁ h => ihb b₁ h);
                 aux ihb b₁ h;
               aux xb acb ihb lt b₁ h Eq₃);
-        aux rfl (Heq.refl xb)
+        aux rfl (HEq.refl xb)
 
 -- The lexicographical order of well founded relations is well-founded
 def lexWf (ha : WellFounded r) (hb : ∀ x, WellFounded (s x)) : WellFounded (Lex r s) :=
diff --git a/src/library/constants.cpp b/src/library/constants.cpp
index 5b508477bd..0d81b5773e 100644
--- a/src/library/constants.cpp
+++ b/src/library/constants.cpp
@@ -114,7 +114,6 @@ name const * g_list_to_array = nullptr;
 name const * g_match_failed = nullptr;
 name const * g_monad = nullptr;
 name const * g_monad_fail = nullptr;
-name const * g_lean_name = nullptr;
 name const * g_lean_name_anonymous = nullptr;
 name const * g_lean_name_num = nullptr;
 name const * g_lean_name_str = nullptr;
@@ -239,7 +238,7 @@ void initialize_constants() {
     g_eq_subst = new name{"Eq", "subst"};
     g_eq_symm = new name{"Eq", "symm"};
     g_eq_trans = new name{"Eq", "trans"};
-    g_eq_of_heq = new name{"eqOfHeq"};
+    g_eq_of_heq = new name{"eqOfHEq"};
     g_eq_true_intro = new name{"eqTrueIntro"};
     g_eq_false_intro = new name{"eqFalseIntro"};
     g_eq_self_iff_true = new name{"eqSelfIffTrue"};
@@ -268,10 +267,10 @@ void initialize_constants() {
     g_has_zero = new name{"HasZero"};
     g_has_zero_zero = new name{"HasZero", "zero"};
     g_has_coe_t = new name{"HasCoeT"};
-    g_heq = new name{"Heq"};
-    g_heq_refl = new name{"Heq", "refl"};
-    g_heq_symm = new name{"Heq", "symm"};
-    g_heq_trans = new name{"Heq", "trans"};
+    g_heq = new name{"HEq"};
+    g_heq_refl = new name{"HEq", "refl"};
+    g_heq_symm = new name{"HEq", "symm"};
+    g_heq_trans = new name{"HEq", "trans"};
     g_heq_of_eq = new name{"heqOfEq"};
     g_huge_fuel = new name{"hugeFuel"};
     g_id = new name{"id"};
@@ -303,7 +302,6 @@ void initialize_constants() {
     g_match_failed = new name{"matchFailed"};
     g_monad = new name{"Monad"};
     g_monad_fail = new name{"MonadFail"};
-    g_lean_name = new name{"Lean", "Name"};
     g_lean_name_anonymous = new name{"Lean", "Name", "anonymous"};
     g_lean_name_num = new name{"Lean", "Name", "num"};
     g_lean_name_str = new name{"Lean", "Name", "str"};
@@ -493,7 +491,6 @@ void finalize_constants() {
     delete g_match_failed;
     delete g_monad;
     delete g_monad_fail;
-    delete g_lean_name;
     delete g_lean_name_anonymous;
     delete g_lean_name_num;
     delete g_lean_name_str;
@@ -682,7 +679,6 @@ name const & get_list_to_array_name() { return *g_list_to_array; }
 name const & get_match_failed_name() { return *g_match_failed; }
 name const & get_monad_name() { return *g_monad; }
 name const & get_monad_fail_name() { return *g_monad_fail; }
-name const & get_lean_name_name() { return *g_lean_name; }
 name const & get_lean_name_anonymous_name() { return *g_lean_name_anonymous; }
 name const & get_lean_name_num_name() { return *g_lean_name_num; }
 name const & get_lean_name_str_name() { return *g_lean_name_str; }
diff --git a/src/library/constants.h b/src/library/constants.h
index 329194664d..a34c0960ec 100644
--- a/src/library/constants.h
+++ b/src/library/constants.h
@@ -116,7 +116,6 @@ name const & get_list_to_array_name();
 name const & get_match_failed_name();
 name const & get_monad_name();
 name const & get_monad_fail_name();
-name const & get_lean_name_name();
 name const & get_lean_name_anonymous_name();
 name const & get_lean_name_num_name();
 name const & get_lean_name_str_name();
diff --git a/src/library/constants.txt b/src/library/constants.txt
index f51defdb79..a0d1f64242 100644
--- a/src/library/constants.txt
+++ b/src/library/constants.txt
@@ -45,7 +45,7 @@ Eq.refl
 Eq.subst
 Eq.symm
 Eq.trans
-eqOfHeq
+eqOfHEq
 eqTrueIntro
 eqFalseIntro
 eqSelfIffTrue
@@ -74,10 +74,10 @@ HasWellFounded.wf
 HasZero
 HasZero.zero
 HasCoeT
-Heq
-Heq.refl
-Heq.symm
-Heq.trans
+HEq
+HEq.refl
+HEq.symm
+HEq.trans
 heqOfEq
 hugeFuel
 id
@@ -109,7 +109,6 @@ List.toArray
 matchFailed
 Monad
 MonadFail
-Lean.Name
 Lean.Name.anonymous
 Lean.Name.num
 Lean.Name.str
diff --git a/stage0/src/library/constants.cpp b/stage0/src/library/constants.cpp
index 5b508477bd..0d81b5773e 100644
--- a/stage0/src/library/constants.cpp
+++ b/stage0/src/library/constants.cpp
@@ -114,7 +114,6 @@ name const * g_list_to_array = nullptr;
 name const * g_match_failed = nullptr;
 name const * g_monad = nullptr;
 name const * g_monad_fail = nullptr;
-name const * g_lean_name = nullptr;
 name const * g_lean_name_anonymous = nullptr;
 name const * g_lean_name_num = nullptr;
 name const * g_lean_name_str = nullptr;
@@ -239,7 +238,7 @@ void initialize_constants() {
     g_eq_subst = new name{"Eq", "subst"};
     g_eq_symm = new name{"Eq", "symm"};
     g_eq_trans = new name{"Eq", "trans"};
-    g_eq_of_heq = new name{"eqOfHeq"};
+    g_eq_of_heq = new name{"eqOfHEq"};
     g_eq_true_intro = new name{"eqTrueIntro"};
     g_eq_false_intro = new name{"eqFalseIntro"};
     g_eq_self_iff_true = new name{"eqSelfIffTrue"};
@@ -268,10 +267,10 @@ void initialize_constants() {
     g_has_zero = new name{"HasZero"};
     g_has_zero_zero = new name{"HasZero", "zero"};
     g_has_coe_t = new name{"HasCoeT"};
-    g_heq = new name{"Heq"};
-    g_heq_refl = new name{"Heq", "refl"};
-    g_heq_symm = new name{"Heq", "symm"};
-    g_heq_trans = new name{"Heq", "trans"};
+    g_heq = new name{"HEq"};
+    g_heq_refl = new name{"HEq", "refl"};
+    g_heq_symm = new name{"HEq", "symm"};
+    g_heq_trans = new name{"HEq", "trans"};
     g_heq_of_eq = new name{"heqOfEq"};
     g_huge_fuel = new name{"hugeFuel"};
     g_id = new name{"id"};
@@ -303,7 +302,6 @@ void initialize_constants() {
     g_match_failed = new name{"matchFailed"};
     g_monad = new name{"Monad"};
     g_monad_fail = new name{"MonadFail"};
-    g_lean_name = new name{"Lean", "Name"};
     g_lean_name_anonymous = new name{"Lean", "Name", "anonymous"};
     g_lean_name_num = new name{"Lean", "Name", "num"};
     g_lean_name_str = new name{"Lean", "Name", "str"};
@@ -493,7 +491,6 @@ void finalize_constants() {
     delete g_match_failed;
     delete g_monad;
     delete g_monad_fail;
-    delete g_lean_name;
     delete g_lean_name_anonymous;
     delete g_lean_name_num;
     delete g_lean_name_str;
@@ -682,7 +679,6 @@ name const & get_list_to_array_name() { return *g_list_to_array; }
 name const & get_match_failed_name() { return *g_match_failed; }
 name const & get_monad_name() { return *g_monad; }
 name const & get_monad_fail_name() { return *g_monad_fail; }
-name const & get_lean_name_name() { return *g_lean_name; }
 name const & get_lean_name_anonymous_name() { return *g_lean_name_anonymous; }
 name const & get_lean_name_num_name() { return *g_lean_name_num; }
 name const & get_lean_name_str_name() { return *g_lean_name_str; }
diff --git a/stage0/src/library/constants.h b/stage0/src/library/constants.h
index 329194664d..a34c0960ec 100644
--- a/stage0/src/library/constants.h
+++ b/stage0/src/library/constants.h
@@ -116,7 +116,6 @@ name const & get_list_to_array_name();
 name const & get_match_failed_name();
 name const & get_monad_name();
 name const & get_monad_fail_name();
-name const & get_lean_name_name();
 name const & get_lean_name_anonymous_name();
 name const & get_lean_name_num_name();
 name const & get_lean_name_str_name();
diff --git a/stage0/src/library/constants.txt b/stage0/src/library/constants.txt
index f51defdb79..a0d1f64242 100644
--- a/stage0/src/library/constants.txt
+++ b/stage0/src/library/constants.txt
@@ -45,7 +45,7 @@ Eq.refl
 Eq.subst
 Eq.symm
 Eq.trans
-eqOfHeq
+eqOfHEq
 eqTrueIntro
 eqFalseIntro
 eqSelfIffTrue
@@ -74,10 +74,10 @@ HasWellFounded.wf
 HasZero
 HasZero.zero
 HasCoeT
-Heq
-Heq.refl
-Heq.symm
-Heq.trans
+HEq
+HEq.refl
+HEq.symm
+HEq.trans
 heqOfEq
 hugeFuel
 id
@@ -109,7 +109,6 @@ List.toArray
 matchFailed
 Monad
 MonadFail
-Lean.Name
 Lean.Name.anonymous
 Lean.Name.num
 Lean.Name.str