1. p : 
2. q : 
3. r : 
  p *q q *q r.nump *q q *q r.den=p *q q *q r.nump *q q *q r.den

By:	RW (LemmaC Thm* x,y:. x=y  x = y) 0

1

p *q q *q r.nump *q q *q r.den = p *q q *q r.nump *q q *q r.den

1 step

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