P:(
Prop). (x:. P(x) 
(
x':. x'<x & P(x'))) 
(x:. P(x))is mentioned by
| P:(Prop). (x:. P(x) (x':. x'<x & P(x'))) (x:. P(x)) | [nat_descent] |
In prior sections: core well fnd int 1 bool 1 rel 1 quot 1 LogicSupplement int 2
Try larger context:
DiscrMathExt
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html