Def (first x  as s.t. P(x) else d)
Def == Case of filter(x.P(x);as); nil  d ; a.b  a

is mentioned by

Thm* P:(T), as:T List, d:T. Thm* ((first a  as s.t. P(a) else d)  as) Thm*  (first a  as s.t. P(a) else d) = d

[find_property]

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