Who Cites fpf-all?
fpf-all	Def xdom(f). v=f(x)   P(x;v) == x:A. x  dom(f)  P(x;f(x))
fpf-ap	Def f(x) == 2of(f)(x)
fpf-dom	Def x  dom(f) == deq-member(eq;x;1of(f))
assert	Def b == if b True else False fi
	Thm* b:. b  Prop
pi2	Def 2of(t) == t.2
	Thm* A:Type, B:(AType), p:(a:AB(a)). 2of(p)  B(1of(p))
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
pi1	Def 1of(t) == t.1
	Thm* A:Type, B:(AType), p:(a:AB(a)). 1of(p)  A
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

Syntax:

xdom(f). v=f(x)   P(x;v)

has structure:

fpf-all(A; eq; f; x,v.P(x;v))

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