Nuprl Basics - Proof: sfa doc fun noteq example1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sfa doc fun noteq example1 1 1

1. (

x.x) = (

x.if x<0

0 ; x fi)
2. -1 = if (-1)<0

0 ; -1 fi

False

By:	Reduce Hyp:-1

Generated subgoal:

1 2. -1 = 0
False
Auto

About:

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