diff --git a/stage0/src/Init/NotationExtra.lean b/stage0/src/Init/NotationExtra.lean
index db24b1a5b7..036912e5fd 100644
--- a/stage0/src/Init/NotationExtra.lean
+++ b/stage0/src/Init/NotationExtra.lean
@@ -60,8 +60,9 @@ end Lean
 
 open Lean
 
-macro "∃"  xs:explicitBinders ", " b:term : term => expandExplicitBinders `Exists xs b
-macro "Σ"  xs:explicitBinders ", " b:term : term => expandExplicitBinders `Sigma xs b
+macro "∃" xs:explicitBinders ", " b:term : term => expandExplicitBinders `Exists xs b
+macro "exists" xs:explicitBinders ", " b:term : term => expandExplicitBinders `Exists xs b
+macro "Σ" xs:explicitBinders ", " b:term : term => expandExplicitBinders `Sigma xs b
 macro "Σ'" xs:explicitBinders ", " b:term : term => expandExplicitBinders `PSigma xs b
 macro:25 xs:bracketedExplicitBinders "×" b:term : term => expandBrackedBinders `Sigma xs b
 macro:25 xs:bracketedExplicitBinders "×'" b:term : term => expandBrackedBinders `PSigma xs b
diff --git a/stage0/src/Lean/Level.lean b/stage0/src/Lean/Level.lean
index 11fe615c52..3ea3298267 100644
--- a/stage0/src/Lean/Level.lean
+++ b/stage0/src/Lean/Level.lean
@@ -418,14 +418,14 @@ instance : ToString Level := ⟨Format.pretty ∘ Level.format⟩
 end Level
 
 /- Similar to `mkLevelMax`, but applies cheap simplifications -/
+@[export lean_level_mk_max_simp]
 def mkLevelMax' (u v : Level) : Level :=
   let subsumes (u v : Level) : Bool :=
-    match u with
-    | Level.max u₁ u₂ _ => v == u₁ || v == u₂
-    | _ => false
-  if u.isExplicit && v.isExplicit then
-    if u.getOffset ≥ v.getOffset then u else v
-  else if u == v then u
+    if v.isExplicit && u.getOffset ≥ v.getOffset then true
+    else match u with
+      | Level.max u₁ u₂ _ => v == u₁ || v == u₂
+      | _ => false
+  if u == v then u
   else if u.isZero then v
   else if v.isZero then u
   else if subsumes u v then u
@@ -436,6 +436,7 @@ def mkLevelMax' (u v : Level) : Level :=
     mkLevelMax u v
 
 /- Similar to `mkLevelIMax`, but applies cheap simplifications -/
+@[export lean_level_mk_imax_simp]
 def mkLevelIMax' (u v : Level) : Level :=
   if v.isNeverZero then mkLevelMax' u v
   else if v.isZero then v
diff --git a/stage0/src/kernel/level.cpp b/stage0/src/kernel/level.cpp
index 90902bcae5..d3adde3eb6 100644
--- a/stage0/src/kernel/level.cpp
+++ b/stage0/src/kernel/level.cpp
@@ -29,6 +29,8 @@ extern "C" object * lean_level_mk_mvar(obj_arg);
 extern "C" object * lean_level_mk_param(obj_arg);
 extern "C" object * lean_level_mk_max(obj_arg, obj_arg);
 extern "C" object * lean_level_mk_imax(obj_arg, obj_arg);
+extern "C" object * lean_level_mk_max_simp(obj_arg, obj_arg);
+extern "C" object * lean_level_mk_imax_simp(obj_arg, obj_arg);
 
 level mk_succ(level const & l) { return level(lean_level_mk_succ(l.to_obj_arg())); }
 level mk_max_core(level const & l1, level const & l2) { return level(lean_level_mk_max(l1.to_obj_arg(), l2.to_obj_arg())); }
@@ -305,7 +307,7 @@ extern "C" object * lean_level_update_max(obj_arg l, obj_arg new_lhs, obj_arg ne
         return l;
     } else {
         lean_dec_ref(l);
-        return lean_level_mk_max(new_lhs, new_rhs);
+        return lean_level_mk_max_simp(new_lhs, new_rhs);
     }
 }
 
@@ -315,7 +317,7 @@ extern "C" object * lean_level_update_imax(obj_arg l, obj_arg new_lhs, obj_arg n
         return l;
     } else {
         lean_dec_ref(l);
-        return lean_level_mk_imax(new_lhs, new_rhs);
+        return lean_level_mk_imax_simp(new_lhs, new_rhs);
     }
 }
 
diff --git a/stage0/stdlib/Init/NotationExtra.c b/stage0/stdlib/Init/NotationExtra.c
index 4b8587c204..16d47ca9b9 100644
--- a/stage0/stdlib/Init/NotationExtra.c
+++ b/stage0/stdlib/Init/NotationExtra.c
@@ -14,11 +14,9 @@
 extern "C" {
 #endif
 lean_object* l_myMacro____x40_Init_NotationExtra___hyg_901____closed__1;
-lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__4;
 size_t l_USize_add(size_t, size_t);
 lean_object* l_Lean_expandExplicitBindersAux_loop___closed__5;
 lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1107____closed__4;
-lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__2;
 lean_object* l_Lean_unbracktedExplicitBinders;
 lean_object* l_Lean_explicitBinders___closed__4;
 lean_object* l___kind_term____x40_Init_NotationExtra___hyg_859____closed__10;
@@ -33,11 +31,13 @@ lean_object* l_Lean_expandExplicitBindersAux(lean_object*, lean_object*, lean_ob
 lean_object* l_Lean_expandBrackedBindersAux_loop_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_myMacro____x40_Init_NotationExtra___hyg_901____boxed(lean_object*, lean_object*, lean_object*);
 extern lean_object* l___kind_term____x40_Init_Notation___hyg_3____closed__13;
+lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__6;
 extern lean_object* l_Array_empty___closed__1;
 lean_object* l_Lean_expandExplicitBindersAux_loop___closed__12;
 lean_object* l_Lean_explicitBinders___closed__2;
 lean_object* l_Lean_expandExplicitBindersAux_loop_match__1(lean_object*);
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_5787____closed__11;
+lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__2;
 lean_object* l_Lean_bracketedExplicitBinders___closed__7;
 lean_object* l_Lean_unbracktedExplicitBinders___closed__4;
 uint8_t lean_name_eq(lean_object*, lean_object*);
@@ -49,19 +49,20 @@ extern lean_object* l_myMacro____x40_Init_Notation___hyg_6031____closed__4;
 lean_object* l___kind_term____x40_Init_NotationExtra___hyg_859____closed__5;
 lean_object* lean_array_push(lean_object*, lean_object*);
 lean_object* lean_array_get_size(lean_object*);
-lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__5;
 lean_object* l_Lean_expandExplicitBindersAux_loop(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_bracketedExplicitBinders___closed__3;
 lean_object* l_Lean_explicitBinders___closed__1;
 lean_object* l_Lean_expandExplicitBindersAux_loop_match__1___rarg(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_expandExplicitBindersAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1393____boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_bracketedExplicitBinders___closed__5;
 lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1107____closed__3;
-lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__3;
 lean_object* l_Lean_expandExplicitBindersAux_loop___closed__13;
 lean_object* l_Lean_expandExplicitBindersAux_loop___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__6;
 lean_object* l_Lean_expandExplicitBindersAux_loop___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___kind_term____x40_Init_NotationExtra___hyg_859____closed__2;
+lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__7;
 lean_object* l_Lean_expandBrackedBindersAux_loop(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_expandBrackedBindersAux_loop___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_expandBrackedBindersAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -71,23 +72,29 @@ lean_object* l_Lean_binderIdent;
 lean_object* l_Lean_expandBrackedBinders(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
 extern lean_object* l_Lean_Name_appendIndexAfter___closed__1;
+lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__3;
 lean_object* lean_nat_sub(lean_object*, lean_object*);
 lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__5;
+lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__5;
 lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__1;
 lean_object* l_Lean_Syntax_copyInfo(lean_object*, lean_object*);
 lean_object* l_Lean_bracketedExplicitBinders___closed__6;
 lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_explicitBinders___closed__5;
 lean_object* l_Array_anyMUnsafe_any___at_Lean_expandExplicitBinders___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1507____boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_expandExplicitBindersAux_loop___closed__7;
 lean_object* l___kind_term____x40_Init_NotationExtra___hyg_983____closed__7;
 lean_object* l_Lean_expandExplicitBinders(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1273____closed__1;
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_6360____closed__17;
+lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1273____boxed(lean_object*, lean_object*, lean_object*);
 extern lean_object* l___private_Init_Util_0__mkPanicMessage___closed__2;
-lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1269____boxed(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_6360____closed__15;
+lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1273____closed__2;
 lean_object* l_Lean_expandBrackedBindersAux_loop_match__1___rarg(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Init_Prelude___instance__72___closed__1;
+lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__4;
 lean_object* l_Lean_bracketedExplicitBinders;
 lean_object* l_Lean_unbracktedExplicitBinders___closed__6;
 lean_object* l_Lean_bracketedExplicitBinders___closed__2;
@@ -95,7 +102,6 @@ lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1025____boxed(lean_object
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_38____closed__8;
 lean_object* l___kind_term____x40_Init_NotationExtra___hyg_983____closed__4;
 lean_object* l_Lean_expandExplicitBindersAux_loop___closed__11;
-lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1025____closed__2;
 lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__6;
 uint8_t l_Array_anyMUnsafe_any___at_Lean_expandExplicitBinders___spec__1(lean_object*, lean_object*, size_t, size_t);
 lean_object* l___kind_term____x40_Init_NotationExtra___hyg_859____closed__6;
@@ -104,13 +110,13 @@ lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__3;
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_6360____closed__13;
 size_t lean_usize_of_nat(lean_object*);
 lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1107____closed__5;
+lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__1;
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_38____closed__6;
 lean_object* l_Lean_bracketedExplicitBinders___closed__1;
 lean_object* l___kind_term____x40_Init_NotationExtra___hyg_859____closed__8;
 lean_object* l_Lean_bracketedExplicitBinders___closed__8;
 extern lean_object* l_Lean_nullKind___closed__2;
 lean_object* l_Lean_bracketedExplicitBinders___closed__9;
-lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1025____closed__1;
 lean_object* l_Lean_bracketedExplicitBinders___closed__4;
 lean_object* l_Lean_expandExplicitBindersAux_loop_match__2___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_expandBrackedBindersAux_loop_match__1(lean_object*);
@@ -121,8 +127,9 @@ lean_object* l_Lean_expandExplicitBindersAux_loop_match__1___rarg___boxed(lean_o
 lean_object* l_Lean_expandExplicitBindersAux_loop___closed__6;
 lean_object* l___kind_term____x40_Init_NotationExtra___hyg_983____closed__6;
 uint8_t lean_nat_dec_le(lean_object*, lean_object*);
+lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1469_;
 lean_object* l___kind_term____x40_Init_NotationExtra___hyg_859_;
-lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1345_;
+lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1355_;
 lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1231_;
 lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1107_;
 lean_object* l___kind_term____x40_Init_NotationExtra___hyg_983_;
@@ -133,17 +140,19 @@ extern lean_object* l_myMacro____x40_Init_Notation___hyg_38____closed__2;
 lean_object* l___kind_term____x40_Init_NotationExtra___hyg_983____closed__5;
 lean_object* l_Lean_unbracktedExplicitBinders___closed__7;
 extern lean_object* l_Lean_Name_hasMacroScopes___closed__1;
-lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1383_(lean_object*, lean_object*, lean_object*);
+lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1393_(lean_object*, lean_object*, lean_object*);
+lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1507_(lean_object*, lean_object*, lean_object*);
 lean_object* l_myMacro____x40_Init_NotationExtra___hyg_901_(lean_object*, lean_object*, lean_object*);
 lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1025_(lean_object*, lean_object*, lean_object*);
 lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1149_(lean_object*, lean_object*, lean_object*);
-lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1269_(lean_object*, lean_object*, lean_object*);
+lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1273_(lean_object*, lean_object*, lean_object*);
 lean_object* l___kind_term____x40_Init_NotationExtra___hyg_859____closed__3;
 lean_object* l_Lean_expandExplicitBindersAux_loop_match__2(lean_object*);
 uint8_t l_Lean_Syntax_isNone(lean_object*);
 lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
 lean_object* l___kind_term____x40_Init_NotationExtra___hyg_859____closed__7;
 lean_object* l_Lean_expandBrackedBindersAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__3;
 lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__2;
 lean_object* l_Lean_expandBrackedBinders___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_binderIdent___closed__4;
@@ -154,6 +163,7 @@ uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*);
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_5787____closed__8;
 lean_object* l_Lean_expandExplicitBindersAux_loop___closed__1;
 extern lean_object* l___kind_term____x40_Init_Notation___hyg_6910____closed__7;
+lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__5;
 lean_object* l_Lean_expandExplicitBindersAux_loop___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_mkHole___closed__2;
 lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1107____closed__1;
@@ -178,11 +188,11 @@ lean_object* l_Lean_unbracktedExplicitBinders___closed__3;
 lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1149____closed__2;
 lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1149____boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_myMacro____x40_Init_NotationExtra___hyg_901____closed__2;
-lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__6;
+lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__4;
 lean_object* l_Lean_unbracktedExplicitBinders___closed__2;
-lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__1;
-lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1383____boxed(lean_object*, lean_object*, lean_object*);
+lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__2;
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_6360____closed__11;
+lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__1;
 lean_object* l_Lean_expandExplicitBindersAux_loop___closed__3;
 lean_object* l___kind_term____x40_Init_NotationExtra___hyg_859____closed__9;
 uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
@@ -1573,7 +1583,7 @@ static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_983____c
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string("Σ");
+x_1 = lean_mk_string("exists");
 return x_1;
 }
 }
@@ -1651,24 +1661,6 @@ x_1 = l___kind_term____x40_Init_NotationExtra___hyg_983____closed__7;
 return x_1;
 }
 }
-static lean_object* _init_l_myMacro____x40_Init_NotationExtra___hyg_1025____closed__1() {
-_start:
-{
-lean_object* x_1; 
-x_1 = lean_mk_string("Sigma");
-return x_1;
-}
-}
-static lean_object* _init_l_myMacro____x40_Init_NotationExtra___hyg_1025____closed__2() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = lean_box(0);
-x_2 = l_myMacro____x40_Init_NotationExtra___hyg_1025____closed__1;
-x_3 = lean_name_mk_string(x_1, x_2);
-return x_3;
-}
-}
 lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1025_(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
@@ -1713,7 +1705,7 @@ x_15 = l_Lean_Syntax_getArg(x_1, x_14);
 x_16 = lean_unsigned_to_nat(3u);
 x_17 = l_Lean_Syntax_getArg(x_1, x_16);
 lean_dec(x_1);
-x_18 = l_myMacro____x40_Init_NotationExtra___hyg_1025____closed__2;
+x_18 = l_myMacro____x40_Init_NotationExtra___hyg_901____closed__2;
 x_19 = l_Lean_expandExplicitBinders(x_18, x_15, x_17, x_2, x_3);
 lean_dec(x_15);
 return x_19;
@@ -1744,7 +1736,7 @@ static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1107____
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string("Σ'");
+x_1 = lean_mk_string("Σ");
 return x_1;
 }
 }
@@ -1826,7 +1818,7 @@ static lean_object* _init_l_myMacro____x40_Init_NotationExtra___hyg_1149____clos
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string("PSigma");
+x_1 = lean_mk_string("Sigma");
 return x_1;
 }
 }
@@ -1915,7 +1907,7 @@ static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1231____
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string("×");
+x_1 = lean_mk_string("Σ'");
 return x_1;
 }
 }
@@ -1934,8 +1926,8 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
 x_1 = l___kind_term____x40_Init_Notation___hyg_3____closed__13;
-x_2 = l_Lean_bracketedExplicitBinders;
-x_3 = l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__3;
+x_2 = l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__3;
+x_3 = l_Lean_explicitBinders;
 x_4 = lean_alloc_ctor(2, 3, 0);
 lean_ctor_set(x_4, 0, x_1);
 lean_ctor_set(x_4, 1, x_2);
@@ -1949,7 +1941,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
 x_1 = l___kind_term____x40_Init_Notation___hyg_3____closed__13;
 x_2 = l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__4;
-x_3 = l___kind_term____x40_Init_Notation___hyg_6293____closed__9;
+x_3 = l___kind_term____x40_Init_Notation___hyg_6910____closed__7;
 x_4 = lean_alloc_ctor(2, 3, 0);
 lean_ctor_set(x_4, 0, x_1);
 lean_ctor_set(x_4, 1, x_2);
@@ -1961,9 +1953,23 @@ static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1231____
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
+x_1 = l___kind_term____x40_Init_Notation___hyg_3____closed__13;
+x_2 = l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__5;
+x_3 = l___kind_term____x40_Init_Notation___hyg_6293____closed__9;
+x_4 = lean_alloc_ctor(2, 3, 0);
+lean_ctor_set(x_4, 0, x_1);
+lean_ctor_set(x_4, 1, x_2);
+lean_ctor_set(x_4, 2, x_3);
+return x_4;
+}
+}
+static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__7() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
 x_1 = l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__1;
-x_2 = lean_unsigned_to_nat(25u);
-x_3 = l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__5;
+x_2 = lean_unsigned_to_nat(1023u);
+x_3 = l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__6;
 x_4 = lean_alloc_ctor(3, 3, 0);
 lean_ctor_set(x_4, 0, x_1);
 lean_ctor_set(x_4, 1, x_2);
@@ -1975,11 +1981,29 @@ static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1231_()
 _start:
 {
 lean_object* x_1; 
-x_1 = l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__6;
+x_1 = l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__7;
 return x_1;
 }
 }
-lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1269_(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+static lean_object* _init_l_myMacro____x40_Init_NotationExtra___hyg_1273____closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string("PSigma");
+return x_1;
+}
+}
+static lean_object* _init_l_myMacro____x40_Init_NotationExtra___hyg_1273____closed__2() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = lean_box(0);
+x_2 = l_myMacro____x40_Init_NotationExtra___hyg_1273____closed__1;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
+lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1273_(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
 lean_object* x_4; uint8_t x_5; 
@@ -2002,7 +2026,7 @@ lean_object* x_8; lean_object* x_9; lean_object* x_10; uint8_t x_11;
 x_8 = l_Lean_Syntax_getArgs(x_1);
 x_9 = lean_array_get_size(x_8);
 lean_dec(x_8);
-x_10 = lean_unsigned_to_nat(3u);
+x_10 = lean_unsigned_to_nat(4u);
 x_11 = lean_nat_dec_eq(x_9, x_10);
 lean_dec(x_9);
 if (x_11 == 0)
@@ -2018,62 +2042,63 @@ return x_13;
 else
 {
 lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; 
-x_14 = lean_unsigned_to_nat(0u);
+x_14 = lean_unsigned_to_nat(1u);
 x_15 = l_Lean_Syntax_getArg(x_1, x_14);
-x_16 = lean_unsigned_to_nat(2u);
+x_16 = lean_unsigned_to_nat(3u);
 x_17 = l_Lean_Syntax_getArg(x_1, x_16);
 lean_dec(x_1);
-x_18 = l_myMacro____x40_Init_NotationExtra___hyg_1025____closed__2;
-x_19 = l_Lean_expandBrackedBinders(x_18, x_15, x_17, x_2, x_3);
+x_18 = l_myMacro____x40_Init_NotationExtra___hyg_1273____closed__2;
+x_19 = l_Lean_expandExplicitBinders(x_18, x_15, x_17, x_2, x_3);
+lean_dec(x_15);
 return x_19;
 }
 }
 }
 }
-lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1269____boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1273____boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
 lean_object* x_4; 
-x_4 = l_myMacro____x40_Init_NotationExtra___hyg_1269_(x_1, x_2, x_3);
+x_4 = l_myMacro____x40_Init_NotationExtra___hyg_1273_(x_1, x_2, x_3);
 lean_dec(x_2);
 return x_4;
 }
 }
-static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__1() {
+static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__1() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l___kind_term____x40_Init_NotationExtra___hyg_859____closed__3;
-x_2 = lean_unsigned_to_nat(1345u);
+x_2 = lean_unsigned_to_nat(1355u);
 x_3 = lean_name_mk_numeral(x_1, x_2);
 return x_3;
 }
 }
-static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__2() {
+static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__2() {
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string("×'");
+x_1 = lean_mk_string("×");
 return x_1;
 }
 }
-static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__3() {
+static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__3() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; 
-x_1 = l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__2;
+x_1 = l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__2;
 x_2 = lean_alloc_ctor(5, 1, 0);
 lean_ctor_set(x_2, 0, x_1);
 return x_2;
 }
 }
-static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__4() {
+static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__4() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
 x_1 = l___kind_term____x40_Init_Notation___hyg_3____closed__13;
 x_2 = l_Lean_bracketedExplicitBinders;
-x_3 = l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__3;
+x_3 = l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__3;
 x_4 = lean_alloc_ctor(2, 3, 0);
 lean_ctor_set(x_4, 0, x_1);
 lean_ctor_set(x_4, 1, x_2);
@@ -2081,12 +2106,12 @@ lean_ctor_set(x_4, 2, x_3);
 return x_4;
 }
 }
-static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__5() {
+static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__5() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
 x_1 = l___kind_term____x40_Init_Notation___hyg_3____closed__13;
-x_2 = l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__4;
+x_2 = l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__4;
 x_3 = l___kind_term____x40_Init_Notation___hyg_6293____closed__9;
 x_4 = lean_alloc_ctor(2, 3, 0);
 lean_ctor_set(x_4, 0, x_1);
@@ -2095,13 +2120,13 @@ lean_ctor_set(x_4, 2, x_3);
 return x_4;
 }
 }
-static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__6() {
+static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__6() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
-x_1 = l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__1;
+x_1 = l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__1;
 x_2 = lean_unsigned_to_nat(25u);
-x_3 = l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__5;
+x_3 = l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__5;
 x_4 = lean_alloc_ctor(3, 3, 0);
 lean_ctor_set(x_4, 0, x_1);
 lean_ctor_set(x_4, 1, x_2);
@@ -2109,19 +2134,19 @@ lean_ctor_set(x_4, 2, x_3);
 return x_4;
 }
 }
-static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1345_() {
+static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1355_() {
 _start:
 {
 lean_object* x_1; 
-x_1 = l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__6;
+x_1 = l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__6;
 return x_1;
 }
 }
-lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1383_(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1393_(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
 lean_object* x_4; uint8_t x_5; 
-x_4 = l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__1;
+x_4 = l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__1;
 lean_inc(x_1);
 x_5 = l_Lean_Syntax_isOfKind(x_1, x_4);
 if (x_5 == 0)
@@ -2168,11 +2193,149 @@ return x_19;
 }
 }
 }
-lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1383____boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1393____boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
 lean_object* x_4; 
-x_4 = l_myMacro____x40_Init_NotationExtra___hyg_1383_(x_1, x_2, x_3);
+x_4 = l_myMacro____x40_Init_NotationExtra___hyg_1393_(x_1, x_2, x_3);
+lean_dec(x_2);
+return x_4;
+}
+}
+static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__1() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l___kind_term____x40_Init_NotationExtra___hyg_859____closed__3;
+x_2 = lean_unsigned_to_nat(1469u);
+x_3 = lean_name_mk_numeral(x_1, x_2);
+return x_3;
+}
+}
+static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__2() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string("×'");
+return x_1;
+}
+}
+static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__3() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__2;
+x_2 = lean_alloc_ctor(5, 1, 0);
+lean_ctor_set(x_2, 0, x_1);
+return x_2;
+}
+}
+static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__4() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
+x_1 = l___kind_term____x40_Init_Notation___hyg_3____closed__13;
+x_2 = l_Lean_bracketedExplicitBinders;
+x_3 = l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__3;
+x_4 = lean_alloc_ctor(2, 3, 0);
+lean_ctor_set(x_4, 0, x_1);
+lean_ctor_set(x_4, 1, x_2);
+lean_ctor_set(x_4, 2, x_3);
+return x_4;
+}
+}
+static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__5() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
+x_1 = l___kind_term____x40_Init_Notation___hyg_3____closed__13;
+x_2 = l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__4;
+x_3 = l___kind_term____x40_Init_Notation___hyg_6293____closed__9;
+x_4 = lean_alloc_ctor(2, 3, 0);
+lean_ctor_set(x_4, 0, x_1);
+lean_ctor_set(x_4, 1, x_2);
+lean_ctor_set(x_4, 2, x_3);
+return x_4;
+}
+}
+static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__6() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
+x_1 = l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__1;
+x_2 = lean_unsigned_to_nat(25u);
+x_3 = l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__5;
+x_4 = lean_alloc_ctor(3, 3, 0);
+lean_ctor_set(x_4, 0, x_1);
+lean_ctor_set(x_4, 1, x_2);
+lean_ctor_set(x_4, 2, x_3);
+return x_4;
+}
+}
+static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1469_() {
+_start:
+{
+lean_object* x_1; 
+x_1 = l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__6;
+return x_1;
+}
+}
+lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1507_(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; uint8_t x_5; 
+x_4 = l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__1;
+lean_inc(x_1);
+x_5 = l_Lean_Syntax_isOfKind(x_1, x_4);
+if (x_5 == 0)
+{
+lean_object* x_6; lean_object* x_7; 
+lean_dec(x_1);
+x_6 = lean_box(1);
+x_7 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_7, 0, x_6);
+lean_ctor_set(x_7, 1, x_3);
+return x_7;
+}
+else
+{
+lean_object* x_8; lean_object* x_9; lean_object* x_10; uint8_t x_11; 
+x_8 = l_Lean_Syntax_getArgs(x_1);
+x_9 = lean_array_get_size(x_8);
+lean_dec(x_8);
+x_10 = lean_unsigned_to_nat(3u);
+x_11 = lean_nat_dec_eq(x_9, x_10);
+lean_dec(x_9);
+if (x_11 == 0)
+{
+lean_object* x_12; lean_object* x_13; 
+lean_dec(x_1);
+x_12 = lean_box(1);
+x_13 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_13, 0, x_12);
+lean_ctor_set(x_13, 1, x_3);
+return x_13;
+}
+else
+{
+lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; 
+x_14 = lean_unsigned_to_nat(0u);
+x_15 = l_Lean_Syntax_getArg(x_1, x_14);
+x_16 = lean_unsigned_to_nat(2u);
+x_17 = l_Lean_Syntax_getArg(x_1, x_16);
+lean_dec(x_1);
+x_18 = l_myMacro____x40_Init_NotationExtra___hyg_1273____closed__2;
+x_19 = l_Lean_expandBrackedBinders(x_18, x_15, x_17, x_2, x_3);
+return x_19;
+}
+}
+}
+}
+lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1507____boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; 
+x_4 = l_myMacro____x40_Init_NotationExtra___hyg_1507_(x_1, x_2, x_3);
 lean_dec(x_2);
 return x_4;
 }
@@ -2316,10 +2479,6 @@ l___kind_term____x40_Init_NotationExtra___hyg_983____closed__7 = _init_l___kind_
 lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_983____closed__7);
 l___kind_term____x40_Init_NotationExtra___hyg_983_ = _init_l___kind_term____x40_Init_NotationExtra___hyg_983_();
 lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_983_);
-l_myMacro____x40_Init_NotationExtra___hyg_1025____closed__1 = _init_l_myMacro____x40_Init_NotationExtra___hyg_1025____closed__1();
-lean_mark_persistent(l_myMacro____x40_Init_NotationExtra___hyg_1025____closed__1);
-l_myMacro____x40_Init_NotationExtra___hyg_1025____closed__2 = _init_l_myMacro____x40_Init_NotationExtra___hyg_1025____closed__2();
-lean_mark_persistent(l_myMacro____x40_Init_NotationExtra___hyg_1025____closed__2);
 l___kind_term____x40_Init_NotationExtra___hyg_1107____closed__1 = _init_l___kind_term____x40_Init_NotationExtra___hyg_1107____closed__1();
 lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1107____closed__1);
 l___kind_term____x40_Init_NotationExtra___hyg_1107____closed__2 = _init_l___kind_term____x40_Init_NotationExtra___hyg_1107____closed__2();
@@ -2352,22 +2511,42 @@ l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__5 = _init_l___kind
 lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__5);
 l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__6 = _init_l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__6();
 lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__6);
+l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__7 = _init_l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__7();
+lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__7);
 l___kind_term____x40_Init_NotationExtra___hyg_1231_ = _init_l___kind_term____x40_Init_NotationExtra___hyg_1231_();
 lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1231_);
-l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__1 = _init_l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__1();
-lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__1);
-l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__2 = _init_l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__2();
-lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__2);
-l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__3 = _init_l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__3();
-lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__3);
-l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__4 = _init_l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__4();
-lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__4);
-l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__5 = _init_l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__5();
-lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__5);
-l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__6 = _init_l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__6();
-lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__6);
-l___kind_term____x40_Init_NotationExtra___hyg_1345_ = _init_l___kind_term____x40_Init_NotationExtra___hyg_1345_();
-lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1345_);
+l_myMacro____x40_Init_NotationExtra___hyg_1273____closed__1 = _init_l_myMacro____x40_Init_NotationExtra___hyg_1273____closed__1();
+lean_mark_persistent(l_myMacro____x40_Init_NotationExtra___hyg_1273____closed__1);
+l_myMacro____x40_Init_NotationExtra___hyg_1273____closed__2 = _init_l_myMacro____x40_Init_NotationExtra___hyg_1273____closed__2();
+lean_mark_persistent(l_myMacro____x40_Init_NotationExtra___hyg_1273____closed__2);
+l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__1 = _init_l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__1();
+lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__1);
+l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__2 = _init_l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__2();
+lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__2);
+l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__3 = _init_l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__3();
+lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__3);
+l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__4 = _init_l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__4();
+lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__4);
+l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__5 = _init_l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__5();
+lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__5);
+l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__6 = _init_l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__6();
+lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__6);
+l___kind_term____x40_Init_NotationExtra___hyg_1355_ = _init_l___kind_term____x40_Init_NotationExtra___hyg_1355_();
+lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1355_);
+l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__1 = _init_l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__1();
+lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__1);
+l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__2 = _init_l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__2();
+lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__2);
+l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__3 = _init_l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__3();
+lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__3);
+l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__4 = _init_l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__4();
+lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__4);
+l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__5 = _init_l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__5();
+lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__5);
+l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__6 = _init_l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__6();
+lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__6);
+l___kind_term____x40_Init_NotationExtra___hyg_1469_ = _init_l___kind_term____x40_Init_NotationExtra___hyg_1469_();
+lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1469_);
 return lean_io_result_mk_ok(lean_box(0));
 }
 #ifdef __cplusplus
diff --git a/stage0/stdlib/Lean/Delaborator.c b/stage0/stdlib/Lean/Delaborator.c
index 88b0c88954..b438f7af86 100644
--- a/stage0/stdlib/Lean/Delaborator.c
+++ b/stage0/stdlib/Lean/Delaborator.c
@@ -1108,7 +1108,6 @@ lean_object* l_Lean_Delaborator_delabInfixOp(lean_object*, lean_object*, lean_ob
 lean_object* l_Lean_Delaborator_delabMul___closed__1;
 extern lean_object* l_Lean_mkOptionalNode___closed__1;
 extern lean_object* l_Array_Init_Data_Array_Basic___instance__3___rarg___closed__1;
-extern lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__2;
 extern lean_object* l___kind_term____x40_Init_Notation___hyg_4833____closed__1;
 extern lean_object* l_Lean_Meta_evalNat___closed__1;
 lean_object* l_Lean_getPPNotation___closed__2;
@@ -1352,6 +1351,7 @@ lean_object* l_Lean_Delaborator_mkDelabAttribute___closed__9;
 lean_object* l_Lean_Level_quote___closed__2;
 lean_object* l_Lean_Delaborator_delabIff___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Delaborator_Lean_Delaborator___instance__4___closed__1;
+extern lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__2;
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_6360____closed__11;
 lean_object* l_Array_zipWithAux___at_Lean_Delaborator_delabAppMatch___spec__4(lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_Array_anyMUnsafe_any___at_Lean_Delaborator_delabLam___spec__1(lean_object*, lean_object*, size_t, size_t);
@@ -27884,7 +27884,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Init_Prelude___instance__72___closed__1;
-x_2 = l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__2;
+x_2 = l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__2;
 x_3 = lean_alloc_ctor(2, 2, 0);
 lean_ctor_set(x_3, 0, x_1);
 lean_ctor_set(x_3, 1, x_2);
diff --git a/stage0/stdlib/Lean/Elab/Level.c b/stage0/stdlib/Lean/Elab/Level.c
index 47fa44b33e..7fd530c87c 100644
--- a/stage0/stdlib/Lean/Elab/Level.c
+++ b/stage0/stdlib/Lean/Elab/Level.c
@@ -50,10 +50,10 @@ extern lean_object* l_Lean_numLitKind;
 lean_object* lean_nat_sub(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Level_mkFreshLevelMVar(lean_object*, lean_object*);
 extern lean_object* l_Lean_Level_LevelToFormat_Result_format___closed__2;
-lean_object* l_Lean_mkLevelMax_x27(lean_object*, lean_object*);
+lean_object* lean_level_mk_max_simp(lean_object*, lean_object*);
 lean_object* l_Lean_replaceRef(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Level_Lean_Elab_Level___instance__3___closed__4;
-lean_object* l_Lean_mkLevelIMax_x27(lean_object*, lean_object*);
+lean_object* lean_level_mk_imax_simp(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Level_elabLevel___closed__12;
 lean_object* l_Lean_Elab_Level_elabLevel_match__2___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Level_elabLevel_match__1(lean_object*);
@@ -728,7 +728,7 @@ lean_inc(x_12);
 x_13 = lean_ctor_get(x_11, 1);
 lean_inc(x_13);
 lean_dec(x_11);
-x_14 = l_Lean_mkLevelIMax_x27(x_4, x_12);
+x_14 = lean_level_mk_imax_simp(x_4, x_12);
 x_15 = 1;
 x_16 = x_3 + x_15;
 x_3 = x_16;
@@ -792,7 +792,7 @@ lean_inc(x_12);
 x_13 = lean_ctor_get(x_11, 1);
 lean_inc(x_13);
 lean_dec(x_11);
-x_14 = l_Lean_mkLevelMax_x27(x_4, x_12);
+x_14 = lean_level_mk_max_simp(x_4, x_12);
 x_15 = 1;
 x_16 = x_3 + x_15;
 x_3 = x_16;
diff --git a/stage0/stdlib/Lean/Level.c b/stage0/stdlib/Lean/Level.c
index dd32f4cb94..4d9af55150 100644
--- a/stage0/stdlib/Lean/Level.c
+++ b/stage0/stdlib/Lean/Level.c
@@ -134,7 +134,7 @@ lean_object* l_Lean_Level_LevelToFormat_Result_format___closed__2;
 uint64_t l_Lean_Level_mkData(size_t, lean_object*, uint8_t, uint8_t);
 lean_object* l_Lean_Level_getLevelOffset_match__1(lean_object*);
 lean_object* lean_level_update_max(lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_mkLevelMax_x27(lean_object*, lean_object*);
+lean_object* lean_level_mk_max_simp(lean_object*, lean_object*);
 lean_object* l_Lean_Level_normalize___closed__1;
 lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
 uint32_t l_UInt64_toUInt32(uint64_t);
@@ -145,7 +145,7 @@ lean_object* l_Lean_Level_ofNat_match__1___rarg___boxed(lean_object*, lean_objec
 lean_object* l___private_Lean_Level_0__Lean_Level_LevelToFormat_formatLst___at_Lean_Level_LevelToFormat_Result_format___spec__2(lean_object*);
 lean_object* l_Lean_Level_occurs_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Level_depth___boxed(lean_object*);
-lean_object* l_Lean_mkLevelIMax_x27(lean_object*, lean_object*);
+lean_object* lean_level_mk_imax_simp(lean_object*, lean_object*);
 lean_object* l_Lean_Level_toNat(lean_object*);
 lean_object* l_Lean_Level_LevelToFormat_Result_max(lean_object*, lean_object*);
 lean_object* l_Lean_Level_normLtAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -5847,42 +5847,45 @@ x_2 = lean_alloc_closure((void*)(l_Lean_mkLevelMax_x27_match__1___rarg), 3, 0);
 return x_2;
 }
 }
-lean_object* l_Lean_mkLevelMax_x27(lean_object* x_1, lean_object* x_2) {
+lean_object* lean_level_mk_max_simp(lean_object* x_1, lean_object* x_2) {
 _start:
 {
-lean_object* x_3; lean_object* x_13; lean_object* x_21; uint8_t x_32; 
-x_32 = l_Lean_Level_isExplicit(x_1);
+lean_object* x_3; lean_object* x_13; uint8_t x_32; 
+x_32 = lean_level_eq(x_1, x_2);
 if (x_32 == 0)
 {
-lean_object* x_33; 
-x_33 = lean_box(0);
-x_21 = x_33;
-goto block_31;
-}
-else
+uint8_t x_33; 
+x_33 = l_Lean_Level_isZero(x_1);
+if (x_33 == 0)
 {
 uint8_t x_34; 
-x_34 = l_Lean_Level_isExplicit(x_2);
+x_34 = l_Lean_Level_isZero(x_2);
 if (x_34 == 0)
 {
-lean_object* x_35; 
-x_35 = lean_box(0);
-x_21 = x_35;
-goto block_31;
-}
-else
+uint8_t x_35; 
+x_35 = l_Lean_Level_isExplicit(x_2);
+if (x_35 == 0)
 {
-lean_object* x_36; lean_object* x_37; lean_object* x_38; uint8_t x_39; 
-x_36 = lean_unsigned_to_nat(0u);
-x_37 = l_Lean_Level_getOffsetAux(x_2, x_36);
-x_38 = l_Lean_Level_getOffsetAux(x_1, x_36);
-x_39 = lean_nat_dec_le(x_37, x_38);
-lean_dec(x_38);
+if (lean_obj_tag(x_1) == 2)
+{
+lean_object* x_36; lean_object* x_37; uint8_t x_38; 
+x_36 = lean_ctor_get(x_1, 0);
+lean_inc(x_36);
+x_37 = lean_ctor_get(x_1, 1);
+lean_inc(x_37);
+x_38 = lean_level_eq(x_2, x_36);
+lean_dec(x_36);
+if (x_38 == 0)
+{
+uint8_t x_39; 
+x_39 = lean_level_eq(x_2, x_37);
 lean_dec(x_37);
 if (x_39 == 0)
 {
-lean_dec(x_1);
-return x_2;
+lean_object* x_40; 
+x_40 = lean_box(0);
+x_13 = x_40;
+goto block_31;
 }
 else
 {
@@ -5890,6 +5893,97 @@ lean_dec(x_2);
 return x_1;
 }
 }
+else
+{
+lean_dec(x_37);
+lean_dec(x_2);
+return x_1;
+}
+}
+else
+{
+lean_object* x_41; 
+x_41 = lean_box(0);
+x_13 = x_41;
+goto block_31;
+}
+}
+else
+{
+lean_object* x_42; lean_object* x_43; lean_object* x_44; uint8_t x_45; 
+x_42 = lean_unsigned_to_nat(0u);
+x_43 = l_Lean_Level_getOffsetAux(x_2, x_42);
+x_44 = l_Lean_Level_getOffsetAux(x_1, x_42);
+x_45 = lean_nat_dec_le(x_43, x_44);
+lean_dec(x_44);
+lean_dec(x_43);
+if (x_45 == 0)
+{
+if (lean_obj_tag(x_1) == 2)
+{
+lean_object* x_46; lean_object* x_47; uint8_t x_48; 
+x_46 = lean_ctor_get(x_1, 0);
+lean_inc(x_46);
+x_47 = lean_ctor_get(x_1, 1);
+lean_inc(x_47);
+x_48 = lean_level_eq(x_2, x_46);
+lean_dec(x_46);
+if (x_48 == 0)
+{
+uint8_t x_49; 
+x_49 = lean_level_eq(x_2, x_47);
+lean_dec(x_47);
+if (x_49 == 0)
+{
+lean_object* x_50; 
+x_50 = lean_box(0);
+x_13 = x_50;
+goto block_31;
+}
+else
+{
+lean_dec(x_2);
+return x_1;
+}
+}
+else
+{
+lean_dec(x_47);
+lean_dec(x_2);
+return x_1;
+}
+}
+else
+{
+lean_object* x_51; 
+x_51 = lean_box(0);
+x_13 = x_51;
+goto block_31;
+}
+}
+else
+{
+lean_dec(x_2);
+return x_1;
+}
+}
+}
+else
+{
+lean_dec(x_2);
+return x_1;
+}
+}
+else
+{
+lean_dec(x_1);
+return x_2;
+}
+}
+else
+{
+lean_dec(x_2);
+return x_1;
 }
 block_12:
 {
@@ -5927,113 +6021,86 @@ return x_1;
 }
 }
 }
-block_20:
+block_31:
 {
+uint8_t x_14; 
 lean_dec(x_13);
+x_14 = l_Lean_Level_isExplicit(x_1);
+if (x_14 == 0)
+{
 if (lean_obj_tag(x_2) == 2)
 {
-lean_object* x_14; lean_object* x_15; uint8_t x_16; 
-x_14 = lean_ctor_get(x_2, 0);
-lean_inc(x_14);
-x_15 = lean_ctor_get(x_2, 1);
+lean_object* x_15; lean_object* x_16; uint8_t x_17; 
+x_15 = lean_ctor_get(x_2, 0);
 lean_inc(x_15);
-x_16 = lean_level_eq(x_1, x_14);
-lean_dec(x_14);
-if (x_16 == 0)
-{
-uint8_t x_17; 
+x_16 = lean_ctor_get(x_2, 1);
+lean_inc(x_16);
 x_17 = lean_level_eq(x_1, x_15);
 lean_dec(x_15);
 if (x_17 == 0)
 {
-lean_object* x_18; 
-x_18 = lean_box(0);
-x_3 = x_18;
-goto block_12;
-}
-else
-{
-lean_dec(x_1);
-return x_2;
-}
-}
-else
-{
-lean_dec(x_15);
-lean_dec(x_1);
-return x_2;
-}
-}
-else
+uint8_t x_18; 
+x_18 = lean_level_eq(x_1, x_16);
+lean_dec(x_16);
+if (x_18 == 0)
 {
 lean_object* x_19; 
 x_19 = lean_box(0);
 x_3 = x_19;
 goto block_12;
 }
+else
+{
+lean_dec(x_1);
+return x_2;
 }
-block_31:
+}
+else
 {
-uint8_t x_22; 
-lean_dec(x_21);
-x_22 = lean_level_eq(x_1, x_2);
-if (x_22 == 0)
+lean_dec(x_16);
+lean_dec(x_1);
+return x_2;
+}
+}
+else
 {
-uint8_t x_23; 
-x_23 = l_Lean_Level_isZero(x_1);
-if (x_23 == 0)
+lean_object* x_20; 
+x_20 = lean_box(0);
+x_3 = x_20;
+goto block_12;
+}
+}
+else
 {
-uint8_t x_24; 
-x_24 = l_Lean_Level_isZero(x_2);
+lean_object* x_21; lean_object* x_22; lean_object* x_23; uint8_t x_24; 
+x_21 = lean_unsigned_to_nat(0u);
+x_22 = l_Lean_Level_getOffsetAux(x_1, x_21);
+x_23 = l_Lean_Level_getOffsetAux(x_2, x_21);
+x_24 = lean_nat_dec_le(x_22, x_23);
+lean_dec(x_23);
+lean_dec(x_22);
 if (x_24 == 0)
 {
-if (lean_obj_tag(x_1) == 2)
+if (lean_obj_tag(x_2) == 2)
 {
 lean_object* x_25; lean_object* x_26; uint8_t x_27; 
-x_25 = lean_ctor_get(x_1, 0);
+x_25 = lean_ctor_get(x_2, 0);
 lean_inc(x_25);
-x_26 = lean_ctor_get(x_1, 1);
+x_26 = lean_ctor_get(x_2, 1);
 lean_inc(x_26);
-x_27 = lean_level_eq(x_2, x_25);
+x_27 = lean_level_eq(x_1, x_25);
 lean_dec(x_25);
 if (x_27 == 0)
 {
 uint8_t x_28; 
-x_28 = lean_level_eq(x_2, x_26);
+x_28 = lean_level_eq(x_1, x_26);
 lean_dec(x_26);
 if (x_28 == 0)
 {
 lean_object* x_29; 
 x_29 = lean_box(0);
-x_13 = x_29;
-goto block_20;
-}
-else
-{
-lean_dec(x_2);
-return x_1;
-}
-}
-else
-{
-lean_dec(x_26);
-lean_dec(x_2);
-return x_1;
-}
-}
-else
-{
-lean_object* x_30; 
-x_30 = lean_box(0);
-x_13 = x_30;
-goto block_20;
-}
-}
-else
-{
-lean_dec(x_2);
-return x_1;
-}
+x_3 = x_29;
+goto block_12;
 }
 else
 {
@@ -6043,13 +6110,29 @@ return x_2;
 }
 else
 {
-lean_dec(x_2);
-return x_1;
+lean_dec(x_26);
+lean_dec(x_1);
+return x_2;
+}
+}
+else
+{
+lean_object* x_30; 
+x_30 = lean_box(0);
+x_3 = x_30;
+goto block_12;
+}
+}
+else
+{
+lean_dec(x_1);
+return x_2;
 }
 }
 }
 }
-lean_object* l_Lean_mkLevelIMax_x27(lean_object* x_1, lean_object* x_2) {
+}
+lean_object* lean_level_mk_imax_simp(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 uint8_t x_3; 
@@ -6093,7 +6176,7 @@ return x_2;
 else
 {
 lean_object* x_8; 
-x_8 = l_Lean_mkLevelMax_x27(x_1, x_2);
+x_8 = lean_level_mk_max_simp(x_1, x_2);
 return x_8;
 }
 }
@@ -6160,7 +6243,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; 
 x_1 = l_Lean_Level_mkData___closed__2;
 x_2 = l_Lean_Level_updateSucc_x21___closed__1;
-x_3 = lean_unsigned_to_nat(464u);
+x_3 = lean_unsigned_to_nat(465u);
 x_4 = lean_unsigned_to_nat(18u);
 x_5 = l_Lean_Level_updateSucc_x21___closed__2;
 x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@@ -6270,7 +6353,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; 
 x_1 = l_Lean_Level_mkData___closed__2;
 x_2 = l_Lean_Level_updateMax_x21___closed__1;
-x_3 = lean_unsigned_to_nat(473u);
+x_3 = lean_unsigned_to_nat(474u);
 x_4 = lean_unsigned_to_nat(21u);
 x_5 = l_Lean_Level_updateMax_x21___closed__2;
 x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@@ -6384,7 +6467,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; 
 x_1 = l_Lean_Level_mkData___closed__2;
 x_2 = l_Lean_Level_updateIMax_x21___closed__1;
-x_3 = lean_unsigned_to_nat(482u);
+x_3 = lean_unsigned_to_nat(483u);
 x_4 = lean_unsigned_to_nat(22u);
 x_5 = l_Lean_Level_updateIMax_x21___closed__2;
 x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@@ -6512,7 +6595,7 @@ x_5 = lean_ctor_get(x_1, 0);
 lean_inc(x_5);
 lean_dec(x_1);
 x_6 = l_Lean_Level_mkNaryMax(x_3);
-x_7 = l_Lean_mkLevelMax_x27(x_5, x_6);
+x_7 = lean_level_mk_max_simp(x_5, x_6);
 return x_7;
 }
 }
diff --git a/stage0/stdlib/Lean/Meta/InferType.c b/stage0/stdlib/Lean/Meta/InferType.c
index 763322a547..921fa77caf 100644
--- a/stage0/stdlib/Lean/Meta/InferType.c
+++ b/stage0/stdlib/Lean/Meta/InferType.c
@@ -114,7 +114,7 @@ lean_object* l_Std_PersistentHashMap_insertAtCollisionNodeAux___at___private_Lea
 lean_object* lean_array_fset(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_whnf___at___private_Lean_Meta_Basic_0__Lean_Meta_forallTelescopeReducingAuxAux_process___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Meta_InferType_0__Lean_Meta_isTypeImp(lean_object*);
-lean_object* l_Lean_mkLevelIMax_x27(lean_object*, lean_object*);
+lean_object* lean_level_mk_imax_simp(lean_object*, lean_object*);
 lean_object* lean_instantiate_type_lparams(lean_object*, lean_object*);
 lean_object* l___private_Lean_Meta_InferType_0__Lean_Meta_isArrowType_match__1(lean_object*);
 lean_object* l_Lean_Meta_isProofQuick_match__1(lean_object*);
@@ -2924,7 +2924,7 @@ lean_inc(x_18);
 x_19 = lean_ctor_get(x_17, 1);
 lean_inc(x_19);
 lean_dec(x_17);
-x_20 = l_Lean_mkLevelIMax_x27(x_18, x_4);
+x_20 = lean_level_mk_imax_simp(x_18, x_4);
 x_2 = x_12;
 x_4 = x_20;
 x_9 = x_19;
diff --git a/stage0/stdlib/Lean/Meta/LevelDefEq.c b/stage0/stdlib/Lean/Meta/LevelDefEq.c
index 994ac313cc..dbf1458072 100644
--- a/stage0/stdlib/Lean/Meta/LevelDefEq.c
+++ b/stage0/stdlib/Lean/Meta/LevelDefEq.c
@@ -145,7 +145,7 @@ lean_object* l___private_Lean_Meta_LevelDefEq_0__Lean_Meta_solve(lean_object*, l
 extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_869____closed__1;
 lean_object* l_Lean_Meta_withoutPostponingUniverseConstraintsImp___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Meta_LevelDefEq_0__Lean_Meta_solveSelfMax(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_mkLevelMax_x27(lean_object*, lean_object*);
+lean_object* lean_level_mk_max_simp(lean_object*, lean_object*);
 lean_object* l___private_Lean_Meta_LevelDefEq_0__Lean_Meta_decAux_x3f_match__4(lean_object*);
 lean_object* l_Lean_Meta_isLevelDefEqAux_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Meta_LevelDefEq_0__Lean_Meta_mkMaxArgsDiff___boxed(lean_object*, lean_object*, lean_object*);
@@ -875,7 +875,7 @@ if (x_32 == 0)
 {
 lean_object* x_33; lean_object* x_34; 
 x_33 = lean_ctor_get(x_23, 0);
-x_34 = l_Lean_mkLevelMax_x27(x_21, x_33);
+x_34 = lean_level_mk_max_simp(x_21, x_33);
 lean_ctor_set(x_23, 0, x_34);
 return x_22;
 }
@@ -885,7 +885,7 @@ lean_object* x_35; lean_object* x_36; lean_object* x_37;
 x_35 = lean_ctor_get(x_23, 0);
 lean_inc(x_35);
 lean_dec(x_23);
-x_36 = l_Lean_mkLevelMax_x27(x_21, x_35);
+x_36 = lean_level_mk_max_simp(x_21, x_35);
 x_37 = lean_alloc_ctor(1, 1, 0);
 lean_ctor_set(x_37, 0, x_36);
 lean_ctor_set(x_22, 0, x_37);
@@ -907,7 +907,7 @@ if (lean_is_exclusive(x_23)) {
  lean_dec_ref(x_23);
  x_40 = lean_box(0);
 }
-x_41 = l_Lean_mkLevelMax_x27(x_21, x_39);
+x_41 = lean_level_mk_max_simp(x_21, x_39);
 if (lean_is_scalar(x_40)) {
  x_42 = lean_alloc_ctor(1, 1, 0);
 } else {
@@ -1067,7 +1067,7 @@ if (x_74 == 0)
 {
 lean_object* x_75; lean_object* x_76; 
 x_75 = lean_ctor_get(x_65, 0);
-x_76 = l_Lean_mkLevelMax_x27(x_63, x_75);
+x_76 = lean_level_mk_max_simp(x_63, x_75);
 lean_ctor_set(x_65, 0, x_76);
 return x_64;
 }
@@ -1077,7 +1077,7 @@ lean_object* x_77; lean_object* x_78; lean_object* x_79;
 x_77 = lean_ctor_get(x_65, 0);
 lean_inc(x_77);
 lean_dec(x_65);
-x_78 = l_Lean_mkLevelMax_x27(x_63, x_77);
+x_78 = lean_level_mk_max_simp(x_63, x_77);
 x_79 = lean_alloc_ctor(1, 1, 0);
 lean_ctor_set(x_79, 0, x_78);
 lean_ctor_set(x_64, 0, x_79);
@@ -1099,7 +1099,7 @@ if (lean_is_exclusive(x_65)) {
  lean_dec_ref(x_65);
  x_82 = lean_box(0);
 }
-x_83 = l_Lean_mkLevelMax_x27(x_63, x_81);
+x_83 = lean_level_mk_max_simp(x_63, x_81);
 if (lean_is_scalar(x_82)) {
  x_84 = lean_alloc_ctor(1, 1, 0);
 } else {
@@ -2104,7 +2104,7 @@ lean_dec(x_8);
 if (x_9 == 0)
 {
 lean_object* x_10; 
-x_10 = l_Lean_mkLevelMax_x27(x_3, x_2);
+x_10 = lean_level_mk_max_simp(x_3, x_2);
 return x_10;
 }
 else
@@ -2116,7 +2116,7 @@ return x_3;
 default: 
 {
 lean_object* x_11; 
-x_11 = l_Lean_mkLevelMax_x27(x_3, x_2);
+x_11 = lean_level_mk_max_simp(x_3, x_2);
 return x_11;
 }
 }
diff --git a/stage0/stdlib/Lean/Util/ReplaceLevel.c b/stage0/stdlib/Lean/Util/ReplaceLevel.c
index 1bf8bb6171..d4515e4325 100644
--- a/stage0/stdlib/Lean/Util/ReplaceLevel.c
+++ b/stage0/stdlib/Lean/Util/ReplaceLevel.c
@@ -33,8 +33,8 @@ lean_object* l_List_map___at_Lean_Expr_replaceLevel___spec__1(lean_object*, lean
 lean_object* l_List_map___at_Lean_Expr_ReplaceLevelImpl_replaceUnsafeM_visit___spec__1(lean_object*, lean_object*);
 lean_object* l_Lean_Level_replace_match__2___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Expr_ReplaceLevelImpl_replaceUnsafeM_visit_match__1(lean_object*);
-lean_object* l_Lean_mkLevelMax_x27(lean_object*, lean_object*);
-lean_object* l_Lean_mkLevelIMax_x27(lean_object*, lean_object*);
+lean_object* lean_level_mk_max_simp(lean_object*, lean_object*);
+lean_object* lean_level_mk_imax_simp(lean_object*, lean_object*);
 lean_object* l_Lean_Expr_ReplaceLevelImpl_replaceUnsafe(lean_object*, lean_object*);
 lean_object* l_Lean_Expr_ReplaceLevelImpl_initCache___closed__1;
 lean_object* lean_expr_update_let(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -188,7 +188,7 @@ lean_dec(x_2);
 lean_inc(x_1);
 x_9 = l_Lean_Level_replace(x_1, x_7);
 x_10 = l_Lean_Level_replace(x_1, x_8);
-x_11 = l_Lean_mkLevelMax_x27(x_9, x_10);
+x_11 = lean_level_mk_max_simp(x_9, x_10);
 return x_11;
 }
 case 3:
@@ -202,7 +202,7 @@ lean_dec(x_2);
 lean_inc(x_1);
 x_14 = l_Lean_Level_replace(x_1, x_12);
 x_15 = l_Lean_Level_replace(x_1, x_13);
-x_16 = l_Lean_mkLevelIMax_x27(x_14, x_15);
+x_16 = lean_level_mk_imax_simp(x_14, x_15);
 return x_16;
 }
 default: