Nuprl Lemma : bind-class-locally-programmable

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

all: x:A. B[x], 

squash: T, 

implies: P  Q, 

function: x:A  B[x], 

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

and: P  Q, 

so_lambda: x.t[x], 

prop: , 

member: t  T, 

exists: x:A. B[x], 

sq_exists: x:{A| B[x]}, 

implies: P  Q, 

all: x:A. B[x], 

squash: T, 

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

assert: b, 

not: A, 

subtype: S  T, 

rev_implies: P  Q, 

iff: P  Q, 

es-le-before: loc(e), 

le: A  B, 

or: P  Q, 

es-le: e loc e' , 

rev_subtype_rel: A r B, 

nat: , 

bag-combine: xbs.f[x], 

le_int: i z j, 

bnot: b, 

lelt: i  j < k, 

int_seg: {i..j}, 

bool: , 

it: