IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
da-outlink-f wf da:k:Knd fp-> Type, k:{k:Knd| k dom(da) & isrcv(k) }.
da-outlink-f(da;k) IdLnkIdType
By:
Auto THEN Unfold `da-outlink-f` 0 THEN Analyze -1
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
da:k:Knd fp-> Type, k:{k:Knd| k 
dom(da) & isrcv(k) }.
da-outlink-f(da;k) 
Id
