is mentioned by

Thm* R:(A(A List)PropProp).  Thm* P:((A List)Prop).  Thm* (P(nil)  Q) & (a:A, x:A List. P(a.x)  R(a,x,P(x)))

[sfa_doc_listind_via_so]

In prior sections: core well fnd int 1 bool 1 rel 1 int 2 list 1 sqequal 1

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