IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
least satisfies1 1. k :
2. p : {p:(k)| i:k. p(i) }
3. (least i:. p(i)) {i:k| p(i) & (j:i. p(j)) }
p(least i:. p(i))
By:
Analyze3 THEN Analyze2 THEN Unhide
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html