Nuprl - Proof: eq rat refl 1 1 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: eq rat refl 1 1 1 1 1

1. x1 :

2. x2 :

x1/x2.num

x1/x2.den = x1/x2.num

x1/x2.den

By:	RWH qnd_evalC 0

Generated subgoal:

1 x1x2 = x1x2
Auto

About:

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