Typehood and Membership

What follows is not a definition but a body of facts easily derived from the definition above.

  T type iff void or atom or int

or (a=b in A) & &

or (a<b) & int & int

or A list & A type

or A|B & A type & B type

or ( x:A#B or A#B )
* & A type & if

or ( x:A->B or A->B )
* & A type & if

or ( {x:A|B} or {A|B} )
* & A type & if

or
* ( x,y:A//B or A//B )
* & A type
* & u,v,w are distinct and don't occur in B
* & u:A->
* & u:A->v:A->->
* & u:A->v:A->w:A->->->
*

or Uk

  if &

not void

atom iff

int iff

(a=b in A) iff axiom &

a<b iff axiom & & & m is less than n

A list iff A list type
* & nil or (a.b) & & A list

A|B iff A|B type
* & ( inl(a) & ) or inr(b) &

x:A#B iff x:A#B type & <a,b> & &

x:A->B iff x:A->B type
* & \ u.b
* &
* if

{x:A|B} iff {x:A|B} type & &

x,y:A//B iff x,y:A//B type &

Uk iff void or atom or int

or (a=b in A) & Uk & &

or (a<b) & int & int

or A list & Uk

or A|B & Uk & Uk

or ( x:A#B or A#B )
* & Uk & Uk if

or ( x:A->B or A->B )
* & Uk & Uk if

or ( {x:A|B} or {A|B} )
* & Uk & Uk if

or
* ( x,y:A//B or A//B )
* & Uk
* & Uk
* if &
* & u,v,w are distinct and don't occur in B
* & u:A->
* & u:A->v:A->->
* & u:A->v:A->w:A->->->
*

or Uj & j is less than k