[Agda] `postulate' in `let'

[Serge D. Mechveliani]

Can you, please, explain the difference of `where' and `let' constructs
with respect to `postulate' ?
Consider the following small program using 
Agda-2.3.0.1 + Standad library lib-0.6
(in which I replace the math symbols with  Nat  and  `subtract'):

------------------------------------------
lessNat? : Nat -> Nat -> Bool  
lessNat? 0       0       = false
lessNat? 0       (suc _) = true
lessNat? (suc _) 0       = false
lessNat? (suc n) (suc m) = lessNat? n m

LessNat? : Nat -> Nat -> Set
LessNat? n m = T (lessNat? n m)

f : (n : Nat) -> LessNat? 7 n -> Nat
f n _ = subtract n 8                  -- subtract = \.-  -- math symbol

g : Nat -> Nat
g n = f m p  where
             m = (n + 3) * (n + 3)
             postulate p : LessNat? 7 m

-- I am testing `postulate' because I imagine for  m  some expression of 
-- which value I am sure that it is greater than 7, and which formal 
-- inequality proof is difficult to provide.

g2 : Nat -> Nat                       -- a variant of  g
g2 n = let m = (n + 3) * (n + 3)
           postulate p : LessNat? 7 m
       in  f m p

h : Nat -> Nat
h n = let L7 : Set           -- just some test example with `let'
          L7 = LessNat? 7 n
          h' : Nat -> Nat
          h' n = n + 2 
      in  h' (n * n)
-------------------------------------------

Now,  g  and  h  are compiled,  
and  g2  is not:
                 "Not a valid let-declaration when scope checking".

What is the meaning of this difference?
Thanks,

------
Sergei