Nuprl Lemma : defined-by-rec-comb-program

int_seg: {i..j}, 

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

all: x:A. B[x], 

lambda: x.A[x], 

function: x:A  B[x], 

fpf-dom: x  dom(f), 

not: A, 

prop: , 

le: A  B, 

so_lambda: x.t[x], 

and: P  Q, 

exists: x:A. B[x], 

implies: P  Q, 

member: t  T, 

all: x:A. B[x], 

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

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

squash: T, 

nat: , 

ge: i  j , 

es-le-before: loc(e), 

subtype: S  T, 

assert: b, 

le_int: i z j, 

bnot: b, 

rev_implies: P  Q, 

iff: P  Q, 

es-le: e loc e' , 

or: P  Q, 

lelt: i  j < k, 

int_seg: {i..j}, 

bool: , 

it: ,