Nuprl Lemma : simple-loc-comb1-concat-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], 

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

nat: , 

member: t  T, 

le: A  B, 

not: A, 

implies: P  Q, 

ge: i  j , 

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

le_int: i z j, 

bnot: b, 

int_seg: {i..j}, 

all: x:A. B[x], 

lelt: i  j < k, 

and: P  Q, 

iff: P  Q, 

rev_implies: P  Q, 

squash: T, 

exists: x:A. B[x], 

eq_int: (i = j), 

prop: , 

so_lambda: x.t[x], 

cand: A c B, 

or: P  Q, 

subtype: S  T