IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
Dconstant compatible loc:Id, T:Type, c:T, x,i:Id. (A,BDconstant(loc;T;c;x;i).A ||+ B)
By:
ProvePairwiseCompatible
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html