Nuprl - Proof: cancel sub

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: cancel sub

x,n,m:

. x

n & x

(nnsub(n;x) = nnsub(m;x)

n = m)

By:	RewriteOfThm Thm: hcancel sub (SimpsetC [`hol_to_nuprl`;`bequal`])

Generated subgoals:

None

About:

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