wList again.

[Serguey Zefirov]

These exercises are just exciting. This is the most interesting
paradigm shift I experienced in 8 years. ;)

Did I described wList
------------------------------------------------------------------------------
     ( a : A ;  b : Bool !        (       a : A        !
data !-------------------!  where !--------------------!
     !    So1 a b : *    )        ! oh1 a : So1 A true )
------------------------------------------------------------------------------
     ( p : So1 A false !
let  !-----------------!
     !  notSo1 p : X   )

     notSo1 p <= case p
------------------------------------------------------------------------------
     (    A : *    !
let  !-------------!
     ! wList A : * )

     wList A => W Bool (So1 A)
------------------------------------------------------------------------------
     ( a : A ;  as : wList A !
let  !-----------------------!
     ! wCons a as : wList A  )

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