Nuprl - Proof: mult clauses

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

m,n:

m = 0

& m

0 = 0

& 1

m = m

& m

1 = m

& (m+1)

n = m

n+n

& m

(n+1) = m+m

By:	RewriteOfThm Thm: hmult clauses (SimpsetC [`hol_to_nuprl`;`bequal`])

Generated subgoals:

None

About:

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