Nuprl - Proof: multiply functionality wrt le 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: multiply functionality wrt le 1

1. i1 :

2. i2 :

3. j1 :

4. j2 :

5. i1

j1
6. i2

By:	Inst: Thm* a,b:, n:. ab nanb Using:[i2 \| j2 \| i1] THEN Inst: Thm* a,b:, n:. ab nanb Using:[i1 \| j1 \| j2]

Generated subgoal:

1 7. i1i2i1j2
8. j2i1j2j1
i1i2j1j2
Auto

About:

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