Def  == Unit+Unit

is mentioned by

Thm* t',m:, T:Type, f:(T), P:(T). Thm* m+1||filter(P;map(f;upto(t')))|| Thm*  Thm* (t:. P(f(t)) & ||filter(P;map(f;upto(t)))|| = m  )	[filter_map_upto2]
Thm* i,j:. Thm* i<j Thm*  Thm* (f:(T), P:(T). Thm* (P(f(i))  ||filter(P;map(f;upto(i)))||<||filter(P;map(f;upto(j)))||)	[filter_map_upto]
Thm* P:(T), A:T List, B:Top. filter(P;A @ B) ~ (filter(P;A) @ filter(P;B))	[filter_append_sq]
Thm* f:(). (n:. f(n))  f(mu(f)) & (i:. i<mu(f)  f(i))	[mu-property]
Thm* f:(). (n:. f(n))  mu(f)	[mu_wf]

In prior sections: bool 1 list 1 sqequal 1 rel 1 mb nat mb list 1 mb list 2

Try larger context: EventSystems IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html