(3steps total) PrintForm Definitions Lemmas int 2 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: multiply functionality wrt le
  i1,i2,j1,j2:. i1j1  i2j2  i1i2j1j2
By: Auto

Generated subgoal:

1 1. i1 : 
2. i2 : 
3. j1 : 
4. j2 : 
5. i1j1
6. i2j2
  i1i2j1j2
2 steps

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

(3steps total) PrintForm Definitions Lemmas int 2 Sections StandardLIB Doc