IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def P Q == (P Q) & (P Q)
is mentioned by
Thm* i:, A:({i...}Prop). (j:. ij A(j)) (j:{i...}. A(j)) | [int_le_to_int_upper] |
Thm* i:, A:({i+1...}Prop). (j:. i<j A(j)) (j:{i+1...}. A(j)) | [int_lt_to_int_upper] |
In prior sections:
core
well fnd
Try larger context:
StandardLIB
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html