Def  == <nil,x.>

is mentioned by

Thm* B,eq,g:Top.   g	[fpf-empty-sub]
Thm* B:(AType), f:x:A fp-> B(x). fpf-is-empty(f)  f =   x:A fp-> B(x)	[assert-fpf-is-empty]

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