Nuprl - Proof: eq rat sym 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. x1 :

2. x2 :

3. y1 :

4. y2 :

5. <x1,x2>.num

<y1,y2>.den=

<y1,y2>.num

<x1,x2>.den

<y1,y2>.num

<x1,x2>.den=

<x1,x2>.num

<y1,y2>.den

By:	OnClauses [0;5] (Unfolds [`qdenom`;`qnumer`]) THEN OnClauses [0;5] (RWH (pi1_evalC ORELSEC pi2_evalC))

Generated subgoal:

1 5. x1y2=y1x2
y1x2=x1y2
2 steps

About:

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