IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
s-pre-init-rule112 1. Id
2. Id
3. x : Id
4. A : Type
5. T : Type
6. A 7. ATProp
State(x : A) Type
By:
Auto THEN Unfold `s-decl` 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html