1. T : Type
2. P : T
3. T List
4. u : T
5. v : T List
6. d:T. 
6. ((first a  v s.t. P(a) else d)  v)  (first a  v s.t. P(a) else d) = d
7. P(u)
  d:T. 
  ((first a  v s.t. P(a) else d)  [u / v])
   (first a  v s.t. P(a) else d) = d

None

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