Nuprl - Proof: two sqr roots 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: two sqr roots 1 1

1. p :

2. q :

3. p

p = 2

p':

. p'<p & (

q':

. p'

p' = 2

q')

By:	Inst: Thm* p:, q:. pp = 2qq (p':. p'<p & qq = 2p'p')

Generated subgoal:

1 4. p:, q:. pp = 2qq (p':. p'<p & qq = 2p'p')
p':. p'<p & (q':. p'p' = 2q'q')
3 steps

About:

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