Nuprl - Proof: atomic char 2 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: atomic char 2 1

1. a :

(a ~ 1)
3. 2 | a

(2 ~ 1)

(2 ~ a)
4. a = 0

False

By:	HypSubst 4 3 THEN Analyze 3

Generated subgoals:

1 3. a = 0
  2 | 0
1 step

2 3. a = 0
4. (2 ~ 1)  (2 ~ 0)
  False
1 step

About:

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

1	3. a = 0 2 \| 0	1 step
2	3. a = 0 4. (2 ~ 1) (2 ~ 0) False	1 step