IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
inj typing imp le1 1. m :
2. k :
3. f : {f:(mk)| Inj(m; k; f) }
Inj(m; k; f)
By:
Analyze-1 THEN Unhide
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html