Nuprl - Proof: rem eq args z

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: rem eq args z

, b:

. |a| = |b|

(a rem b) = 0

By:	SimilarTo a:, b:. \|a\| = \|b\| (a rem b) = 0

Generated subgoals:

1 1. a :
2. b :
3. |a| = |b|
  (a rem b) = 0
3 steps

2 1. a :
2. b:. |a| = |b|  (a rem b) = 0
3. b :
4. |a| = |b|
  (a rem b) = 0
4 steps

About:

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

1	1. a : 2. b : 3. \|a\| = \|b\| (a rem b) = 0	3 steps
2	1. a : 2. b:. \|a\| = \|b\| (a rem b) = 0 3. b : 4. \|a\| = \|b\| (a rem b) = 0	4 steps