Nuprl - Proof: mul cancel in eq

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: mul cancel in eq

a,b:

, n:

. n

a = n

a = b

By:	SimilarTo a,b:, n:. na = nb a = b

Generated subgoals:

1 1. a :
2. b :
3. n :
4. na = nb
  a = b
2 steps

2 1. a :
2. b :
3. n:. na = nb  a = b
4. n :
5. na = nb
  a = b
3 steps

About:

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

1	1. a : 2. b : 3. n : 4. na = nb a = b	2 steps
2	1. a : 2. b : 3. n:. na = nb a = b 4. n : 5. na = nb a = b	3 steps