IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hexists unique def11 1. 'a : S
(p:'a. b_exists_unique('a;x.p(x)))
=
(P:'a. (x:'a. (P(x)))(x,y:'a. ((P(x))(P(y)))(x =y)))
By:
Unab [`b_exists_unique`] THEN Simp THEN StrongAuto
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(
p:'a
. b_exists_unique('a;x.p(x)))
=
x:'a. (P(x)))
(
