Nuprl - Proof: sub cancel

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

x,n,m:

. n

x & m

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

n = m)

By:	RewriteOfThm Thm: hsub cancel (SimpsetC [`hol_to_nuprl`;`bequal`])

Generated subgoals:

None

About:

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