Def  == Unit+Unit

is mentioned by

Thm* (n.n<0) = (n.false)	[sfa_doc_sqtype_ctr_example_part2]
Thm* P:(AProp). (x:A. Dec(P(x)))  (f:(A). x:A. P(x)  f(x))	[sfa_doc_bool_vs_decidable_fun]
Thm* Dec(P)  (b:. P  b)	[sfa_doc_bool_vs_decidable]
Thm* i:. i even	[sfa_doc_even_wf]
Thm* f:{f:()| x:. f(x) }, i:. i<mu(f)  f(i)	[kleene_minimize_is_lb]
Thm* f:{f:()| x:. f(x) }. f(mu(f))	[kleene_minimize_is_fp]
Thm* mu  {f:()| x:. f(x) }	[kleene_minimize_wf]
Thm* f:{f:()| x:. f(x) }. f(0)  (x.f(1+x))  {f:()| x:. f(x) }	[kleene_tail]

In prior sections: bool 1 rel 1 list 1 sqequal 1

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