Improve an example in Basics/Namespace and modules

[DanielRrr]

The tutorial says

Each definition can be accompanied by \where block in the end. 
In contrast to Haskell, \where block is attached to the whole definition, not to a particular clause:

\func f => g \where \func g => 0

But this example doesn’t seem helpful in terms of demonstrating this feature of Arend. I would give an alternative example here. The Haskell definition of f would be exactly the same (modulo its syntax), so it’s worth giving an example containing many blocks. For example, the following is accepted in Haskell:

foo :: Int -> Int
foo 0 = bar 1
  where
  bar x = x + 2
foo n = bar (n + 2)
  where
  bar x = x + 2

Whereas the following is rejected since bar is not in scope in the first equation

foo :: Int -> Int
foo 0 = bar 1
foo n = bar (n + 2)
  where
  bar x = x + 2

But this is accepted in Arend:

\func foo (x : Nat) : Nat \elim x
  | 0 => bar 1
  | n => bar (n + 2)
    \where \func bar (x : Nat) => x + 2

This foo is off the top of my head, but it demonstrates that feature of Arend a bit better in my opinion.