Nuprl Lemma : iterated_classrel_invariant3

prior_iterated_classrel: s  prior(X*(f,init,e)), 

classrel: v  X(e), 

es-le: e loc e' , 

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

prop: , 

all: x:A. B[x], 

implies: P  Q, 

function: x:A  B[x], 

bag-member: x  bs, 

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

so_lambda: x.t[x], 

not: A, 

le: A  B, 

ge: i  j , 

nat: , 

squash: T, 

member: t  T, 

all: x:A. B[x], 

implies: P  Q, 

prop: , 

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

cand: A c B, 

and: P  Q, 

or: P  Q, 

prior_iterated_classrel: s  prior(X*(f,init,e)), 

es-le: e loc e' , 

exists: x:A. B[x], 

subtype: S  T