Nuprl - int_1 LEMMAs for comp_nat_ind_a

int 1 Sections StandardLIB Doc

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

Theorem	Name
Thm* P:(Prop). (i:. (j:. j<i P(j)) P(i)) (i:. P(i))	[comp_nat_ind_a]
cites the following:
Thm* P:(Prop). P(0) (i:. P(i-1) P(i)) (i:. P(i))	[nat_ind_a]

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

int 1 Sections StandardLIB Doc