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

2 steps

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