Who Cites fpf-compatible?
fpf-compatible	Def f || g == x:A. x  dom(f) & x  dom(g)  f(x) = g(x)  B(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:

f || g

has structure:

fpf-compatible(A; a.B(a); eq; f; g)

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