Nuprl - Proof: divides instance 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: divides instance 1 1

1. ext{decidable__divides}(3,6)

(3 | 6

3 | 6)

3 | 6

By:	(UseWitness outl(ext{decidable__divides}(3,6))) THEN Analyze

Generated subgoals:

1 ext{decidable__divides}(3,6) (3 | 6)+(3 | 6)
Trivial

2 isl(ext{decidable__divides}(3,6))
1 step

About:

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

1	ext{decidable__divides}(3,6) (3 \| 6)+(3 \| 6)	Trivial
2	isl(ext{decidable__divides}(3,6))	1 step