Why there are explicit p:So (...) in
( u : A ; us : UniqList A eq xs ; p : So (not (elem u xs eq)) !
!---------------------------------------------------------------!
! ulCons u us p : UniqList A eq (cons x xs) )? I, actually, tried to make it implicit, but failed. And I cannot figure why.
