Update a bit more

theories/Core/Soundness/Weakening/Lemmas.v

@@ -79,7 +79,7 @@ Proof with mautosolve.
     eapply weakening_resp_equiv; [mauto 2 |].
     transitivity {{{ Id ∘ σ0 }}}...
   - eapply wk_p; eauto.
-    transitivity {{{ Wk ∘ τ ∘ σ0 }}}; mauto 4.
+    transitivity {{{ (Wk ∘ τ) ∘ σ0 }}}; mauto 4.
     eapply wf_sub_eq_compose_assoc; revgoals...
 Qed.
 

theories/Core/Syntactic/Syntax.v

@@ -126,41 +126,42 @@ Open Scope mcltt_scope.
 (** ** Syntactic Notations *)
 Module Syntax_Notations.
   Notation "{{{ x }}}" := x (at level 0, x custom exp at level 99, format "'{{{'  x  '}}}'") : mcltt_scope.
+  (** We need to define substitution notation first to assert [left associativity] of level 0. *)
+  Notation "e [ s ]" := (a_sub e s) (in custom exp at level 0, e custom exp, s custom exp at level 60, left associativity, format "e [ s ]") : mcltt_scope.
   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 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 "'λ' A e" := (a_fn A e) (in custom exp at level 1, A custom exp at level 0, 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 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 "'Type' @ n" := (a_typ n) (in custom exp at level 0, n constr at level 0, format "'Type' @ n") : mcltt_scope.
+  Notation "'Π' A B" := (a_pi A B) (in custom exp at level 1, A custom exp at level 0, 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 1, e custom exp at level 1) : mcltt_scope.
+  Notation "'succ' e" := (a_succ e) (in custom exp at level 1, e custom exp at level 0) : 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 "'#' n" := (a_var n) (in custom exp at level 0, n constr at level 0, format "'#' n") : mcltt_scope.
   Notation "'Id'" := a_id (in custom exp at level 0) : mcltt_scope.
   Notation "'Wk'" := a_weaken (in custom exp at level 0) : mcltt_scope.
 
-  Infix "∘" := a_compose (in custom exp at level 40) : mcltt_scope.
-  Infix ",," := a_extend (in custom exp at level 50) : mcltt_scope.
+  Notation "σ ∘ τ" := (a_compose σ τ) (in custom exp at level 40, right associativity, format "σ ∘ τ") : mcltt_scope.
+  Notation "σ ,, e" := (a_extend σ e) (in custom exp at level 50, left associativity, format "σ ,, e") : mcltt_scope.
   Notation "'q' σ" := (q σ) (in custom exp at level 30) : mcltt_scope.
 
   Notation "⋅" := nil (in custom exp at level 0) : mcltt_scope.
-  Notation "x , y" := (cons y x) (in custom exp at level 50) : mcltt_scope.
+  Notation "x , y" := (cons y x) (in custom exp at level 50, format "x ,  y") : mcltt_scope.
 
   Notation "n{{{ x }}}" := x (at level 0, x custom nf at level 99, format "'n{{{'  x  '}}}'") : mcltt_scope.
   Notation "( x )" := x (in custom nf at level 0, x custom nf at level 60) : mcltt_scope.
   Notation "~ x" := x (in custom nf at level 0, x constr at level 0) : mcltt_scope.
   Notation "x" := x (in custom nf at level 0, x ident) : mcltt_scope.
-  Notation "'λ' A e" := (nf_fn A e) (in custom nf at level 0, A custom nf at level 0, e custom nf at level 60) : mcltt_scope.
+  Notation "'λ' A e" := (nf_fn A e) (in custom nf at level 2, A custom nf at level 1, e custom nf at level 60) : mcltt_scope.
   Notation "f x .. y" := (ne_app .. (ne_app f x) .. y) (in custom nf at level 40, f custom nf, x custom nf at next level, y custom nf at next level) : mcltt_scope.
   Notation "'ℕ'" := nf_nat (in custom nf) : mcltt_scope.
-  Notation "'Type' @ n" := (nf_typ n) (in custom nf at level 0, n constr at level 0) : mcltt_scope.
-  Notation "'Π' A B" := (nf_pi A B) (in custom nf at level 0, A custom nf at level 0, B custom nf at level 60) : mcltt_scope.
+  Notation "'Type' @ n" := (nf_typ n) (in custom nf at level 0, n constr at level 0, format "'Type' @ n") : mcltt_scope.
+  Notation "'Π' A B" := (nf_pi A B) (in custom nf at level 2, A custom nf at level 1, B custom nf at level 60) : mcltt_scope.
   Notation "'zero'" := nf_zero (in custom nf at level 0) : mcltt_scope.
-  Notation "'succ' M" := (nf_succ M) (in custom nf at level 0, M custom nf at level 0) : mcltt_scope.
+  Notation "'succ' M" := (nf_succ M) (in custom nf at level 2, M custom nf at level 1) : mcltt_scope.
   Notation "'rec' M 'return' A | 'zero' -> MZ | 'succ' -> MS 'end'" := (ne_natrec A MZ MS M) (in custom nf at level 0, A custom nf at level 60, MZ custom nf at level 60, MS custom nf at level 60, M custom nf at level 60) : mcltt_scope.
-  Notation "'#' n" := (ne_var n) (in custom nf at level 0, n constr at level 0) : mcltt_scope.
-  Notation "'⇑' M" := (nf_neut M) (in custom nf at level 0, M custom nf at level 0) : mcltt_scope.
+  Notation "'#' n" := (ne_var n) (in custom nf at level 0, n constr at level 0, format "'#' n") : mcltt_scope.
+  Notation "'⇑' M" := (nf_neut M) (in custom nf at level 0, M custom nf at level 99, format "'⇑'  M") : mcltt_scope.
 End Syntax_Notations.