Def s == f:'a  'b  'c. g:'a  'b. x:'a. f(x,g(x))

is mentioned

In prior sections: hol combin

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html