Who Cites deq-member?
deq-member	Def deq-member(eq;x;L) == reduce(a,b. eqof(eq)(a,x)  b;false;L)
eqof	Def eqof(d) == 1of(d)
	Thm* T:Type, d:EqDecider(T). eqof(d)  TT
bor	Def p  q == if p true else q fi
	Thm* p,q:. (p  q)
reduce	Def reduce(f;k;as) == Case of as; nil  k ; a.as'  f(a,reduce(f;k;as')) Def (recursive)
	Thm* A,B:Type, f:(ABB), k:B, as:A List. reduce(f;k;as)  B
pi1	Def 1of(t) == t.1
	Thm* A:Type, B:(AType), p:(a:AB(a)). 1of(p)  A

Syntax:

deq-member(eq;x;L)

has structure:

deq-member(eq; x; L)

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html