IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
prime nat11 1. x : 2. prime(x)
3. x = 0
4. (x ~ 1)
5. a:. a | x (a ~ 1) (a ~ x)
2x
By:
x = 1 Asserted THEN SimilarTo: (x ~ 1)
THEN
BackThru: Thm*a,b:. (a ~ b) a = b
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
x = 0
a:
. a | x 
(a ~ 1) 
(a ~ x)
2
x
