(sorry for probable accidental unfinished post)
These exercises are exciting. They shift my paradigm far, far away. ;)
Did I described wList correctly now?
If so, I still cannot get construction like wCons a as => Sup true
(lam p => as). Right now it's beyond my comprehension.
------------------------------------------------------------------------------
( 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 : * !
let !----------------!
! wNil : wList A )
wNil => Sup false notSo1
------------------------------------------------------------------------------
( a : A ; as : wList A !
let !-----------------------!
! wCons a as : wList A )
wCons a as => Sup true (lam p => as)
------------------------------------------------------------------------------
