Def and == p:. q:. pq

is mentioned by

Thm* 'b,'a:S. all(f:'a  'b. and(equal(o(i,f),f),equal(o(f,i),f)))

[hi_o_id]

In prior sections: hol bool

Try larger context: HOLlib IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html