IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
decidable rset equal1 1. R : Id 2. x : Id
3. R(x)
4. y : Id
5. R(y)
6. x = y x = y {i:Id| R(i) }
By:
StrongHypSubst -1 0 THEN Analyze THEN HypSubst -1 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
x = y 
{i:Id| R(i) }
