IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
prime elim1 1. p : 2. prime(p)
3. p = 0
4. (p ~ 1)
5. reducible(p)
6. a : 7. a | p (a ~ 1) (a ~ p)
By:
(Unfold `reducible` 5) THEN (RWW "not_over_and not_over_exists dneg_elim_a" 5)
p = 0
(a ~ 1) 
(a ~ p)
b,c:
. (b ~ 1) 
c
