[Epigram] Generic programming again, now exercise 3.

[Serguey Zefirov]

I decided to start from something lighter than BTree. I choosed a
List. This is easy because Lists are very like Nats, just a little bit
more polymorphic.

When I meditated on that exercise I come to interesting conclusion.
wNat has a "type" *, and has a value from "universe of types", W Bool
So. Does it mean that when we declare wZero : wNat, wNat gets
"expanded" and its' value gets substituted as the type for wZero?

My description of Lists follows wNat example from paper. Did I
described Lists correctly?

------------------------------------------------------------------------------
let  (----------!
     ! wNat : * )

     wNat => W Bool So
------------------------------------------------------------------------------
let  (--------------!
     ! wZero : wNat )

     wZero => Sup false notSo
------------------------------------------------------------------------------
     (   n : wNat    !
let  !---------------!
     ! wSuc n : wNat )

     wSuc n => Sup true (lam p => n)
------------------------------------------------------------------------------
     ( A : * ;  a : A !
let  !----------------!
     !  wList a : *   )

     wList a => W Bool So
------------------------------------------------------------------------------
     (      a : A       !
let  !------------------!
     ! wNil a : wList a )

     wNil a => Sup false notSo
------------------------------------------------------------------------------
     ( a : A ;  as : wList A !
let  !-----------------------!
     ! wCons a as : wList A  )

     wCons a as => Sup true (lam p => as)
------------------------------------------------------------------------------