( set := [U | UNIV][T : U] T -> Prop )
( set_in := [U | UNIV][T | U][P : (set T)][x : T] (P x) )
( set_nil := [U | UNIV][T | U][x : T] False )
( set_full := [U | UNIV][T | U][x : T] True )

( done )