Nuprl - Proof: eq rat sym 1 1 1 1

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

1. x1 :

2. x2 :

3. y1 :

4. y2 :

5. x1

y2=

x2=

By:	OnMClauses [0;5] (RW (LemmaC Thm* x,y:. x=y x = y))

Generated subgoal:

1 5. x1y2 = y1x2
y1x2 = x1y2
Auto

About:

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