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

da || d2

<k,l> = <k1,l1>

ma-single-sends(ds; da; k; l; f) ||+ ma-single-sends(d1; d2; k1; l1; f1)
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