Nuprl - Proof: nsub mul 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: nsub mul 1 1

1. b :

2. c :

3. 0

b = c

(

b) ~

By:	BackThru: Thm* (A ~ 0) (A)

Generated subgoal:

1 ((0b))
1 step

About:

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