Nuprl Lemma : simple-loc-comb1-classrel

classrel: v  X(e), 

uall: [x:A]. B[x], 

exists: x:A. B[x], 

squash: T, 

and: P  Q, 

function: x:A  B[x], 

member: t  T, 

so_lambda: x y.t[x; y], 

so_lambda: x.t[x], 

and: P  Q, 

nat: , 

int_seg: {i..j}, 

le: A  B, 

not: A, 

implies: P  Q, 

lelt: i  j < k, 

ge: i  j , 

le_int: i z j, 

bnot: b, 

all: x:A. B[x], 

subtype: S  T, 

iff: P  Q, 

rev_implies: P  Q, 

eq_int: (i = j), 

uall: [x:A]. B[x], 

exists: x:A. B[x], 

squash: T, 

bag-member: x  bs, 

prop: , 

or: P  Q,