Fix grammar so that sub notation is printed

theories/Core/Soundness/LogicalRelation/CoreLemmas.v

@@ -828,7 +828,7 @@ Proof.
       deepexec H1 ltac:(fun H => pose proof H).
       autorewrite with mcltt in *.
       repeat eexists; eauto.
-      assert {{ Δ0 ⊢s σ0,,N : Δ, ~ (a_sub IT σ) }}.
+      assert {{ Δ0 ⊢s σ0,,N : Δ, IT[σ] }}.
       {
         econstructor; mauto 2.
         bulky_rewrite.

theories/Core/Syntactic/Syntax.v

@@ -129,14 +129,14 @@ Module Syntax_Notations.
   Notation "( x )" := x (in custom exp at level 0, x custom exp at level 60) : mcltt_scope.
   Notation "~ x" := x (in custom exp at level 0, x constr at level 0) : mcltt_scope.
   Notation "x" := x (in custom exp at level 0, x ident) : mcltt_scope.
-  Notation "e [ s ]" := (a_sub e s) (in custom exp at level 0, s custom exp at level 60) : mcltt_scope.
-  Notation "'λ' A e" := (a_fn A e) (in custom exp at level 0, A custom exp at level 0, e custom exp at level 60) : mcltt_scope.
+  Notation "e [ s ]" := (a_sub e s) (in custom exp at level 1, e custom exp, s custom exp at level 60, left associativity, format "e [ s ]") : mcltt_scope.
+  Notation "'λ' A e" := (a_fn A e) (in custom exp at level 1, A custom exp at level 1, e custom exp at level 60) : mcltt_scope.
   Notation "f x .. y" := (a_app .. (a_app f x) .. y) (in custom exp at level 40, f custom exp, x custom exp at next level, y custom exp at next level) : mcltt_scope.
   Notation "'ℕ'" := a_nat (in custom exp) : mcltt_scope.
-  Notation "'Type' @ n" := (a_typ n) (in custom exp at level 0, n constr at level 0) : mcltt_scope.
-  Notation "'Π' A B" := (a_pi A B) (in custom exp at level 0, A custom exp at level 0, B custom exp at level 60) : mcltt_scope.
+  Notation "'Type' @ n" := (a_typ n) (in custom exp at level 1, n constr at level 0) : mcltt_scope.
+  Notation "'Π' A B" := (a_pi A B) (in custom exp at level 1, A custom exp at level 1, B custom exp at level 60) : mcltt_scope.
   Notation "'zero'" := a_zero (in custom exp at level 0) : mcltt_scope.
-  Notation "'succ' e" := (a_succ e) (in custom exp at level 0, e custom exp at level 0) : mcltt_scope.
+  Notation "'succ' e" := (a_succ e) (in custom exp at level 1, e custom exp at level 1) : mcltt_scope.
   Notation "'rec' e 'return' A | 'zero' -> ez | 'succ' -> es 'end'" := (a_natrec A ez es e) (in custom exp at level 0, A custom exp at level 60, ez custom exp at level 60, es custom exp at level 60, e custom exp at level 60) : mcltt_scope.
   Notation "'#' n" := (a_var n) (in custom exp at level 0, n constr at level 0) : mcltt_scope.
   Notation "'Id'" := a_id (in custom exp at level 0) : mcltt_scope.