IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
assert of b exists unique 'a:Type, p:('a).
b_exists_unique('a;x.p(x)) (x:'a. p(x)) & (x,y:'a. p(x) & p(y) x = y)
By:
Unab [`b_exists_unique`] THEN Simp THEN Simp THEN StrongAuto THEN HypBackchain
THEN
StrongAuto
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
'a:Type, p:('a
).
b_exists_unique('a;x.p(x)) 
(
x:'a. p(x)) & (
