Def ij == ji

is mentioned by

Thm* l:A List. ||l||1  ||tl(l)|| = ||l||-1	[length_tl]
Thm* A:Type, l:A List. ||l||1  hd(l)  A	[hd_wf]
Thm* as:A List. as = nil  ||as||1	[length_of_not_nil]
Thm* l:A List. l = nil  ||l||1	[pos_length]
Thm* l:A List. ||l||0	[non_neg_length]

In prior sections: int 2

Try larger context: StandardLIB IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html