IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
uni sat imp in uni set11 1. T : Type
2. a : T 3. Q : TProp
4. Q(a)
5. a':T. Q(a') a' = a 6. y : T 7. Q(y)
y = a
By:
BackThru 5
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Prop
a':T. Q(a') 
a' = a
y = a
