Nuprl - Proof: hzero rep def

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hzero rep def

equal(zero_rep,select(

x:hind. all(

y:hind. not(equal(x,suc_rep(y))))))

By:	HN THEN StrongAuto THEN Unab [`hzero_rep`] THEN HN THEN StrongAuto

Generated subgoal:

1 (@x:. (y:. x = suc_rep(y) )) = (@x:. (y:. (x = (suc_rep(y)))))
1 step

About:

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html