Put heap_lang's let/lambda/rec at level 200.

Coq also uses level 200 for these constructs.
Besides, heap_lang's match and if were also already at this level.

theories/heap_lang/notation.v

@@ -75,10 +75,10 @@ Notation "e1 <- e2" := (Store e1%E e2%E) (at level 80) : expr_scope.
 (* The breaking point '/  ' makes sure that the body of the rec is indented
 by two spaces in case the whole rec does not fit on a single line. *)
 Notation "'rec:' f x := e" := (Rec f%bind x%bind e%E)
-  (at level 102, f at level 1, x at level 1, e at level 200,
+  (at level 200, f at level 1, x at level 1, e at level 200,
    format "'[' 'rec:'  f  x  :=  '/  ' e ']'") : expr_scope.
 Notation "'rec:' f x := e" := (locked (RecV f%bind x%bind e%E))
-  (at level 102, f at level 1, x at level 1, e at level 200,
+  (at level 200, f at level 1, x at level 1, e at level 200,
    format "'[' 'rec:'  f  x  :=  '/  ' e ']'") : val_scope.
 Notation "'if:' e1 'then' e2 'else' e3" := (If e1%E e2%E e3%E)
   (at level 200, e1, e2, e3 at level 200) : expr_scope.
@@ -88,19 +88,19 @@ are stated explicitly instead of relying on the Notations Let and Seq as
 defined above. This is needed because App is now a coercion, and these
 notations are otherwise not pretty printed back accordingly. *)
 Notation "'rec:' f x y .. z := e" := (Rec f%bind x%bind (Lam y%bind .. (Lam z%bind e%E) ..))
-  (at level 102, f, x, y, z at level 1, e at level 200,
+  (at level 200, f, x, y, z at level 1, e at level 200,
    format "'[' 'rec:'  f  x  y  ..  z  :=  '/  ' e ']'") : expr_scope.
 Notation "'rec:' f x y .. z := e" := (locked (RecV f%bind x%bind (Lam y%bind .. (Lam z%bind e%E) ..)))
-  (at level 102, f, x, y, z at level 1, e at level 200,
+  (at level 200, f, x, y, z at level 1, e at level 200,
    format "'[' 'rec:'  f  x  y  ..  z  :=  '/  ' e ']'") : val_scope.
 
 (* The breaking point '/  ' makes sure that the body of the λ: is indented
 by two spaces in case the whole λ: does not fit on a single line. *)
 Notation "λ: x , e" := (Lam x%bind e%E)
-  (at level 102, x at level 1, e at level 200,
+  (at level 200, x at level 1, e at level 200,
    format "'[' 'λ:'  x ,  '/  ' e ']'") : expr_scope.
 Notation "λ: x y .. z , e" := (Lam x%bind (Lam y%bind .. (Lam z%bind e%E) ..))
-  (at level 102, x, y, z at level 1, e at level 200,
+  (at level 200, x, y, z at level 1, e at level 200,
    format "'[' 'λ:'  x  y  ..  z ,  '/  ' e ']'") : expr_scope.
 
 (* When parsing lambdas, we want them to be locked (so as to avoid needless
@@ -110,21 +110,20 @@ printed too. We achieve that by first defining the non-locked notation, and then
 the locked notation. Both will be used for pretty-printing, but only the last
 will be used for parsing. *)
 Notation "λ: x , e" := (LamV x%bind e%E)
-  (at level 102, x at level 1, e at level 200,
+  (at level 200, x at level 1, e at level 200,
    format "'[' 'λ:'  x ,  '/  ' e ']'") : val_scope.
 Notation "λ: x , e" := (locked (LamV x%bind e%E))
-  (at level 102, x at level 1, e at level 200,
+  (at level 200, x at level 1, e at level 200,
    format "'[' 'λ:'  x ,  '/  ' e ']'") : val_scope.
 Notation "λ: x y .. z , e" := (LamV x%bind (Lam y%bind .. (Lam z%bind e%E) .. ))
-  (at level 102, x, y, z at level 1, e at level 200,
+  (at level 200, x, y, z at level 1, e at level 200,
    format "'[' 'λ:'  x  y  ..  z ,  '/  ' e ']'") : val_scope.
 Notation "λ: x y .. z , e" := (locked (LamV x%bind (Lam y%bind .. (Lam z%bind e%E) .. )))
-  (at level 102, x, y, z at level 1, e at level 200,
+  (at level 200, x, y, z at level 1, e at level 200,
    format "'[' 'λ:'  x  y  ..  z ,  '/  ' e ']'") : val_scope.
 
-
 Notation "'let:' x := e1 'in' e2" := (Lam x%bind e2%E e1%E)
-  (at level 102, x at level 1, e1, e2 at level 200,
+  (at level 200, x at level 1, e1, e2 at level 200,
    format "'[' 'let:'  x  :=  '[' e1 ']'  'in'  '/' e2 ']'") : expr_scope.
 Notation "e1 ;; e2" := (Lam BAnon e2%E e1%E)
   (at level 100, e2 at level 200,