[nv-vn]

I think maybe the key idea I was missing here is that the type of a variable is not always the same as the type of the scope it was defined in? If I'm understanding correctly, there's an implicit rule that's missing:

    a : la   b : lb   a := b
   --------------------------
             a : lb

So for example if `b : lb`:

   a := b :>>
   doSomething()

need not have a type `>= lb`.

Does that sound vaguely correct?

Btw thanks for clarifying