IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
ma-single-effect-ma-single-sends-compatible
k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Type, f:(Id
Top) List,
x:Id, k1:Knd, d1:x:Id fp-> Type, d2:a:Knd fp-> Type, f1:Top.
ds || d1

da || d2

ma-single-effect(d1; d2; k1; x; f1) ||+ ma-single-sends(ds; da; k; l; f)
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html