Attempts a reasonable universal closure of the term using the full window term as a context. May also permute some quantifiers to adjust for dependencies.
Intended to be used repeatedly-- after each use, fill in some slots and try again.
See `adj'. IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html