Def false == inr()

is mentioned by

Def deq-member(eq;x;L) == reduce(a,b. eqof(eq)(a,x)  b;false;L)	[deq-member]
Def sumdeq(a;b)(p,q) Def == InjCase(p; pa. InjCase(q; qa. 1of(a)(pa,qa); qb. false); pb. Def == InjCase(q; qa. false; qb. 1of(b)(pb,qb)))	[sumdeq]

In prior sections: bool 1 sqequal 1 list 1 union mb basic

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